FORMAL METHODS IN SOFTWARE ENGINEERING

Catalog description

In the high consequence system domain, a primary objective of any construction technique employed is to provide sufficiently convincing evidence that the system, if put into operation, will not experience a high consequence failure or that the likelihood of such a failure falls within acceptable probabilistically defined limits. Systems for which such evidence can be provided are called high assurance systems. The objective of this course is to examine software-engineering techniques across the development life cycle that are appropriate for high assurance systems. The course will analyze the nature of the evidence provided by various techniques (e.g., does a given technique provide sufficiently strong evidence in a given setting).