Pattern solutions for software and architectures have significantly reduced design, verification, and validation times by mapping challenging problems into a solved generic problem. In the paper, we present an architecture pattern for ensuring synchronous computation semantics using the PALS protocol. We develop a modeling framework in AADL to automatically transform a synchronous design of a real-time distributed system into an asynchronous design satisfying the PALS protocol. We present a detailed example of how the PALS transformation works for a dual-redundant system. From the example, we also describe the general transformation in terms of intuitively defined AADL semantics. Furthermore, we develop a static analysis checker to find necessary conditions that must be satisfied in order for the PALS transformation to work correctly. The transformations and static checks that we have described are implemented in OSATE using the generated EMF metamodel API for model manipulation.

In black-box testing, one is interested in creating a suite of tests from requirements that adequately exercise the behavior of a software system without regard to the internal structure of the implementation. In current practice, the adequacy of black box test suites is inferred by examining coverage on an executable artifact, either source code or a software model.In this paper, we define structural coverage metrics directly on high-level formal software requirements. These metrics provide objective, implementation-independent measures of how well a black-box test suite exercises a set of requirements. We focus on structural coverage criteria on requirements formalized as LTL properties and discuss how they can be adapted to measure finite test cases. These criteria can also be used to automatically generate a requirements-based test suite. Unlike model or code-derived test cases, these tests are immediately traceable to high-level requirements. To assess the practicality of our approach, we apply it on a realistic example from the avionics domain.

Informal requirements stated in a natural language often suffer from ambiguity, inconsistency, and incompleteness. For these reasons, the trend over the last decade has been towards the development of alternate approaches for specifying requirements such as use cases and requirement modeling languages. However, the growing popularity of model-based development and the increasing power of formal verification tools make yet another approach possible. In this approach, informal shall statements are captured as a first step in requirements elicitation. Next, an executable model of the system is constructed that is believed to implement these requirements. Simulation of this model is used to obtain early validation of the requirements with the customer and among the developers. The informal shall statements are then rewritten as formal properties over the model and shown to hold on the model. When possible, this is done through mathematical proof using model-checking or theorem proving. When formal proof is not possible, testing of the properties against the model is used. Finally, source code is automatically generated from the model. For safety or security systems, test cases are also automatically generated from the model and used to check that the object-code executing on the target platform correctly implements the model