Abstract The use of formal methods to prove the correctness of compositional embedded systems is increasingly important. However, the required models and algorithms can induce an enormous complexity. Our approach divides the formal system model into layers and these in turn into modules with defined interfaces, so that reduced formal models can be created for the verification of concrete functional and non-functional requirements. In this work, we use Uppaal to (1) model an RTOS kernel in a modular way and formally specify its internal requirements, (2) model abstract tasks that trigger all kernel functionalities in all combinations or scenarios, and (3) verify the resulting system with regard to task synchronization, resource management, and timing. The result is a fully verified model of the operating system layer that can henceforth serve as a dependable foundation for verifying compositional applications w.r.t. various aspects, such as timing or liveness.

Formalising requirements has the potential to solve problems arising from deficiencies in natural language descriptions. While behavioural requirements are rarely described formally in industry, increasing complexity and new safety standards have renewed the interest in formal specifications. The goal of this paper is to explore how behavioural requirements for embedded systems can be formalised and aligned with verification tasks. Over the course of a 2.5-year project with industry, we modelled existing requirements from a safety-critical automotive software function in several iterations. Taking practical limitations and stakeholder preferences into account, we explored the use of models on different abstraction levels. The final model was used to generate test cases and was evaluated in three interviews with relevant industry practitioners. We conclude that models on a high level of abstraction are most suitable for industrial requirements engineering, especially when they need to be interpreted by other stakeholders.

Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.

We propose a framework for requirement-driven test generation that combines contract-based interface theories with model-based testing. We design a specification language, requirement interfaces, for formalizing different views (aspects) of synchronous data-flow systems from informal requirements. Various views of a system, modeled as requirement interfaces, are naturally combined by conjunction. We develop an incremental test generation procedure with several advantages. The test generation is driven by a single requirement interface at a time. It follows that each test assesses a specific aspect or feature of the system, specified by its associated requirement interface. Since we do not explicitly compute the conjunction of all requirement interfaces of the system, we avoid state space explosion while generating tests. However, we incrementally complete a test for a specific feature with the constraints defined by other requirement interfaces. This allows catching violations of any other requirement during test execution, and not only of the one used to generate the test. This framework defines a natural association between informal requirements, their formal specifications, and the generated tests, thus facilitating traceability. Finally, we introduce a fault-based test-case generation technique, called model-based mutation testing, to requirement interfaces. It generates a test suite that covers a set of fault models, guaranteeing the detection of any corresponding faults in deterministic systems under test. We implemented a prototype test generation tool and demonstrate its applicability in two industrial use cases.

Timed Automata are established specification models for real-time systems. One of their main advantages is composability, allowing the modular specification of different aspects of a system via communicating timed automata. Composed together, these automata specify the behavior of a whole component or system. In previous work, we developed a technique to determinize a single timed automaton, by unfolding it and bounding ourselves to an observable depth k. Within this paper we expand our approach, enabling the efficient bounded determinization of networks of timed automata. We realize an on-the-fly algorithm that performs at each level of unfolding the following tasks: building the product, hiding the communication, removing silent transitions, and determinizing. In contrast to the previous work, this on-the-fly algorithm only needs to traverse the state-space exactly once. We implemented the algorithm in the model-based testing tool MoMuT::TA and demonstrate and evaluate our implementation on a case study.

A lot of systems nowadays, especially in safety-critical areas, have to comply to very strict real-time requirements. Deviation from the specified time behavior can lead to severe faults. Thus the components need to be thoroughly tested to ensure a high quality standard. Model-based testing is a popular technology for automatic and systematic test-case generation, where a system-under-test is tested for conformance with a model that specifies its intended behavior. Model-based mutation testing is a specific fault-oriented variant of model- based testing. In this variant of testing, the test case generation is guided by a mutant, an intentionally altered version of the original model that specifies a common modeling error, to generate a specific test case capable of identifying that error. In the presented thesis we investigate ways to apply model-based mutation testing to real-time applications. The plan is to investigate two specification languages: timed automata and timed contracts. We already developed an algorithm and an implementation for testing deterministic timed automata and a theory and implementation for untimed contracts. In the last year of the thesis we will concentrate on determinizing timed automata restricted to the bounded case, supporting the test-case generation from networks of timed automata and adding real-time support to our contract-based testing tool. The final step of the thesis will be the evaluation on industrial case studies.

In this paper we propose the combination of several techniques into an agile formal development process: model-based testing, formal models, refinement of models, model checking, and test-driven development. The motivation is a smooth integration of formal techniques into an existing development cycle. Formal models are used to generate abstract test cases. These abstract tests are verified against requirement properties by means of model checking. The motivation for verifying the tests and not the model is two-fold: (1) in a typical safety-certification process the test cases are essential, not the models, (2) many common modelling tools do not provide a model checker. We refine the models, check refinement, and generate additional test cases capturing the newly added details. The final refinement step from a model to code is done with classical test-driven development. Hence, a developer implements one generated and formally verified test case after another, until all tests pass. The process is scalable to actual needs. Emphasis can be shifted between formal refinement of models and test-driven development. A car alarm system serves as a demonstrating case-study. We use Back's Action Systems as modelling language and mutation analysis for test case generation. We define refinement as input-output conformance (ioco). Model checking is done with the CADP toolbox.

Europe's industry in embedded system design is currently aiming for a better integration of tools that support their development, validation and verification processes. The idea is to combine model-driven development with model-based testing and model-based analysis. The interoperability of tools shall be achieved with the help of meta-models that facilitate the mapping between different modelling notations. However, the syntactic and semantic integration of tools is a complex and costly task. A common problem is that different tools support different subsets of a language. Furthermore, semantic differences are a major obstacle to sound integration efforts. In this paper we advocate an alternative, more pragmatic approach. We propose the exchange of test cases generated from the models instead of exchanging the models themselves. The advantage is that test cases have a much simpler syntax and semantics, and hence, the mapping between different tools is easier to implement and to maintain. With a formal testing approach with adequate testing criteria a set of test cases can be viewed as partial models that can be formally analysed. We demonstrate an integration of our test case generator Ulysses with the CADP toolbox by means of test case exchange. We generate test cases in Ulysses and verify properties in CADP. We also generate test cases in CADP and perform a mutation analysis in Ulysses.