Jump to ContentJump to Main Navigation
Formal Verification of Control System Software$
Users without a subscription are not able to see the full content.

Pierre-Loïc Garoche

Print publication date: 2019

Print ISBN-13: 9780691181301

Published to Princeton Scholarship Online: January 2020

DOI: 10.23943/princeton/9780691181301.001.0001

Show Summary Details
Page of

PRINTED FROM PRINCETON SCHOLARSHIP ONLINE (www.princeton.universitypressscholarship.com). (c) Copyright Princeton University Press, 2020. All Rights Reserved. An individual user may print out a PDF of a single chapter of a monograph in PRSO for personal use.date: 19 February 2020

Formal Methods

Formal Methods

Different Approaches for Verification

Chapter:
(p.7) Chapter Two Formal Methods
Source:
Formal Verification of Control System Software
Author(s):

Pierre-Loïc Garoche

Publisher:
Princeton University Press
DOI:10.23943/princeton/9780691181301.003.0002

This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to evaluate whether the program they developed fulfills its needs, formal methods are less known and may require a little introduction to the non-expert. This chapter thus serves as a reasonable introduction to the control expert engineer. It first defines the semantics of programs: their basic properties and their meaning. Then, the chapter outlines different formal verifications and explains how they reason on the program artifact. A last part addresses the soundness of the analyses with respect to the actual semantics.

Keywords:   formal methods, verification, control expert engineer, formal verifications, program artifact, critical embedded systems

Princeton Scholarship Online requires a subscription or purchase to access the full text of books within the service. Public users can however freely search the site and view the abstracts and keywords for each book and chapter.

Please, subscribe or login to access full text content.

If you think you should have access to this title, please contact your librarian.

To troubleshoot, please check our FAQs , and if you can't find the answer there, please contact us.