High Assurance Concurrent Software is application software that will perform according to important properties of its specification under abnormal circumstances. Important properties for concurrent programs include safety and liveliness properties, fault tolerance, and security.
Software engineering provides one of the most important techniques, program verification, as a way of showing, formally, that a program satisfies these particular properties with respect to its specification. However, most verification methods do not, in of themselves, account for changes in the running system due to failures or reconfiguration.
Executable assertions, embedded into a distributed computing system, can provide this run-time assurance by checking properties of the program specification at run time. However, generation of these assertions for distributed memory systems is not straightforward. This talk discusses using formal methods of Software Engineering to operationally evaluate a program's proof outline (in both axiomatic and temporal specifications) in a faulty distributed environment to provide necessary run-time assurance.