ACE Assurance, Composed, and Explained
The state-of-the-art in systems assurance is based on testing, simulation and certification, and it is currently incorporating formal verification for some of the system’s components. Formal verification has a limited use at present because it calls for a clean slate design and development, which are not always possible or practical, and because it is computationally challenging for large systems. Therefore, formal verification is commonly constrained to single software or hardware components that can be adequately modeled. Testing and simulation are employed to evaluate the system’s behavior in its environment while targeting large coverage. However, the selection of testing and simulation conditions is manual and prone to human bias of what “worst conditions” mean for the system. Also, the embodiment of the system in an environment can cause problems that were not considered in the design phase, e.g. due to hidden assumptions.
Our goal is to assess the assurance and the risk of safety-critical systems during their entire life-cycle and within the realm of current standard practices. We consider large and complex systems that contain a mixture of legacy and formally verified components. Because of the high complexity, these systems require compositional assurance and risk assessment, and the assurance arguments of engineers are commonly associated with uncertainties. Also, assured components and contracts stemming from external sources cannot be fully trusted in general, and these systems suffer from the emergence of assurance issues and risks due to system integration.
To meet the goal mentioned above we are developing ACE, a new principled approach to quantify and expose the assurance of safety-critical systems across all their components while considering multiple aspects of the system that need to be assured. For this, we are developing a framework for probabilistic assurance and risk evaluation of component-based systems that utilizes information from multiple sources of evidence. The framework supports the argumentation assessment based on experts’ decision and confidence in the decision for the lowest level claims of the arguments. The framework also extends the contracts of system components with “emergent assumptions” that are discovered during simulation, testing and analysis, in an effort to make the implementation’s assumptions explicit. With this approach, we expect to achieve an automated risk assessment of systems that is general, practical and robust.
ACE’s mathematical framework can be used throughout the system’s design and development phase to maintain an updated overview of the system’s assurance and risk assessment: at design time, by merging results from component verification; during development, by merging input from build systems and code analysis tools, and during testing and simulation, by merging results from test and simulation runs. This continuous evaluation will benefit stake-holders by providing system engineers with an “assurance heat map” of the system where “risk hotspots” are identified and can be used to concentrate verification and validation efforts by guiding design and implementation improvement, supporting the isolation and solution of errors, and assisting in strategic decisions. We are aiming to close the loop between traditional engineering and formal methods to better assess the cost/risk trade-off of system assurance.
We evaluate the feasibility of ACE on two use cases: a programmable control system for mobile industrial robots, and an open-source flight controller firmware.
Gustavo A. Quirós is a Senior Scientist at Siemens Corporate Technology. He specializes in industrial automation and has a background in software systems engineering, object-oriented software engineering, programming language design and implementation, software verification, computer networks, distributed systems, and discrete-event simulation. He obtained summa cum laude and the Borchers-Badge of RWTH Aachen University for his doctoral dissertation “Model-based Decentralized Automatic Management of Product Flow Paths in Processing Plants”. He also obtained the NAMUR Award “Process Automation” 2010 from the User Association of Automation Technology in Process Industries.