Arguments about the safety, security, and correctness of a complex system are often made in the form of an assurance case. An assurance case is a structured argument, often represented with a graphical interface, that presents and supports claims about a system's behavior. The argument may combine different kinds of evidence to justify its top level claim. While assurance cases deliver some level of guarantee of a system's correctness, they lack the rigor that proofs from formal methods typically provide. Furthermore, changes in the structure of a model during development may result in inconsistencies between a design and its assurance case. Our solution is a framework for automatically generating assurance cases based on 1) a system model specified in an architectural design language, 2) a set of logical rules expressed in a domain specific language that we have developed, and 3) the results of other formal analyses that have been run on the model. We argue that the rigor of these automatically generated assurance cases exceeds those of traditional assurance case arguments because of their more formal logical foundation and direct connection to the architectural model.
The Evidential Tool Bus (ETB) @cite_10 is very similar in syntax and semantics to Resolute. It is supported by a Datalog-style logic and is designed to combine evidence from a variety of sources. However, the focus of the ETB is on distribution and on provenance ---that is, to log the sequence of tool invocations that were performed to solve the query. It uses timestamps to determine which analyses are out of date with respect to the current development artifacts and to only re-run those analyses that are not synchronized with the current development artifacts. In addition, it is designed to perform distributed execution of analyses. Analysis tool plug-ins are used to execute the analysis tools within ETB. ETB is designed to be tool and model agnostic, and is therefore not integrated with a model of the system architecture.
@cite_10
2238711819
Formal and semi-formal tools are now being used in large projects both for development and certification. A typical project integrates many diverse tools such as static analyzers, model checkers, test generators, and constraint solvers. These tools are usually integrated in an ad hoc manner. There is, however, a need for a tool integration framework that can be used to systematically create workflows, to generate claims along with supporting evidence, and to maintain the claims and evidence as the inputs change. We present the Evidential Tool Bus ETB as a tool integration framework for constructing claims supported by evidence. ETB employs a variant of Datalog as a met alanguage for representing claims, rules, and evidence, and as a scripting language for capturing distributed workflows. ETB can be used to develop assurance cases for certifying complex systems that are developed and assured using a range of tools. We describe the design and prototype implementation of the ETB architecture, and present examples of formal verification workflows defined using ETB.