Dynamic modeling and verification of safe-set architectures

Increased use of software in safety-critical systems has created the need to adequately validate the design and implementation of these systems. Current practice depends on extensive testing which is limited in terms of effectiveness and is very costly. Formal methods have been difficult to apply to the wide range of system architectures and have seldom addressed the system´s dynamic characteristics and behaviour in the presence of faults. Recent developments in formalization of software architecture, definition of safe-set run-time standards and the availability of modeling and analytical tools, make it possible to formally model practical applications that are constrained by well-defined architectures and run-time environments. In particular, the Dynamic Flowgraph Methodology (DFM), developed to model safety-related behaviours of nuclear reactor and aerospace control systems, is especially promising when applied to properly constrained environments. Toolsets to model the architecture and the worst-case schedulability of tasking provide supporting methods. System safety analysis methodologies such as DFM, used in concert with these other developments, provide increased confidence in the validation of safety-critical, software intensive systems. Tools which are available to support DFM, are a graphic model editor with an integrated database and an analysis engine. Schedulability analysis is supported by a Rate Monotonic Analysis (RMA) toolset and a safe-set architecture has been implemented by an Ada run-time environment conforming to the Ada standard