SAE International Integrating Formal Model Checking with the RTEdge\u2122 AADL Microkernel 2011-01-2531

Edgewater Computer Systems Inc. product RTEdge\u2122 Platform 1.2 is a software toolset supporting proof-based engineering, implementation and deployment of software components, built using the RTEdge\u2122 AADL Microkernel modeling subset. This is a small subset of the AADL component model and execution semantics, covering threads and thread-groups communicating solely through asynchronous event ports and through explicitly shared data ports. Threads behavior is expressed as state machines and dispatch run time semantics is encoded in a Run-time Executive, enforcing pre-emptive priority dispatch based on statically assigned event priorities, with ceiling priority protocol access to shared data. This simple AADL microkernel semantic core can support all dispatch policies, communication and synchronization mechanisms of a fully fledged AADL run time environment, permitting the systematic use of the RTEdge\u2122 static analysis tools for AADL-compliant software components. The objective of our work was to integrate RTEdge\u2122 Platform 1.2 with the Promela/Spin (www. spinroot.com) model checker, for the purpose enabling formal verification of user-defined formal properties, expressed on software application models built and executed on the RTEdge\u2122 AADL Microkernel. In order to deal with the state space explosion problem, Model Checking relies on abstractions. Human intervention is required in an error prone process of defining the right abstractions, implementing an equivalent abstracted model in the model checker formalism, proving or disproving a property by model checking and applying the findings to the implementation. Assume-Guarantee Compositional Verification provides both a state space "divide" and "conquer" strategy and a model checking automation strategy, in a reverse engineering process applied to existing component implementations, as an iterative process of assumption refinement by model checking. The RTEdge\u2122 concepts of Protocols, Capsule Interfaces and Composite Capsules open the possibility of using Assume-Guarantee contracts as a specification mechanism, in a forward engineering manner, and of verifying their consistence and conformance by the systematic use of Model Checking. Such an approach would allow verifying very large state spaces by using hierarchical component abstractions formally maintained in the RTEdge\u2122 AADL component model via the "extends" and "implements" refinement relationships. To that end, Protocols, Capsule Interfaces and Composite Capsules must have a compact and convenient way of specifying sets of legal sequences of Signal Events. We developed a set of requirements for adapting IEEE1850 Property Specification Language (PSL) to formally express RTEdge\u2122 software component temporal properties. The adapted PSL will use RTEdge\u2122 Protocols Signals and Data as the underlying vocabulary of the PSL Boolean layer.