Affordable Run-Time V&V of Flight Critical Systems
Verification and validation (V&V)
in distributed systems is a difficult task that is requires
significant cost and effort. Our approach uses formalized attributes
that are available as selectable and enforceable properties
necessary for V&V of critical software. Using this information, two
strategies are proposed. The first uses executable assertions to
verify at run-time that proof conditions are intact. This can be
used for compositional strategies involving proof conditions. The
second method provides an efficient fault tolerant middleware
service to monitor the enforcement of these properties.
The V2 extension to the EDICT tool suite with run-time services.
Completed
verification, validation, fault tolerant, run-time