Formal Methods, and in particular Model Checking, are seeing an increasing use in the Aerospace domain. In recent years, Formal Methods are now commonly used to verify systems and software and its correctness as a way to augment traditional methods relying on simulation and testing. Recent updates to the relevant Aerospace regulations (e.g. DO178C, DO331 and DO333) now have explicit provisions for utilization of models and formal methods. At the system level, Model Checking has seen more limited uses due to the complexity and abstractions needed. In this paper we propose several methods to increase the capability of applying Model Checking to complex Aerospace Systems. An aircraft electrical power system is used to highlight the methodology. Automated model-based methods such as Cone of Influence and Timer Abstractions are described. Results of those simplifications, in combination with traditional Assume-Guarantee approaches will be shown for the Electric Power System application.

The design of large scale complex systems demands the ability to correctly specify and verify as early as possible in the design cycle the interaction of the different components that ensure that the global level requirements are satisfied. We address this issue using an approach based on the notion of contract. In particular, we propose a graphical and text-based language for requirement definition that allows designers to incrementally and hierarchically construct contract specifications for system components by composing a set of simple and intuitive patterns. The patterns have a formal semantics, and are implemented as monitor components in the Simulink framework for runtime verification. The contracts are simulated together with the components to verify both satisfaction and compatibility. A cruise control case study demonstrates the effectiveness of the approach.

In this paper we present Parallel NuSMV, a tool based on the NuSMV model checker that integrates the ManySAT parallel SAT solver. The PNuSMV is part of the FormalSpecs Verifier framework for the formal verification of Simulink/Stateflow models. The experiments we performed show that the use of a parallel SAT solver allows for an average speedup of an order of magnitude or more on industry-level size models. The main contributions of the papers are (1) the description of the PNuSMV model checker (2) the description of the verification time speedup w.r.t. the NuSMV tool for the verification of industrial-sized embedded systems and (3) the integration of the tool in the FormalSpecs Verifier framework for the verification of Simulink/Stateflow models with the application to a cruise control case study.

We present the mathematical foundations and the design methodology of the contract-based model developed in the framework of the SPEEDS project. SPEEDS aims at developing methods and tools to support "speculative design", a design methodology in which distributed designers develop different aspects of the overall system, in a concurrent but controlled way. Our generic mathematical model of contract supports this style of development. This is achieved by focusing on behaviors, by supporting the notion of "rich component" where diverse (functional and non-functional) aspects of the system can be considered and combined, by representing rich components via their set of associated contracts, and by formalizing the whole process of component composition.

We present the mathematical formalism and the verification methodology of the contract-based model developed in the framework of the SPEEDS project. SPEEDS aims at developing methods and tools to support ldquospeculative designrdquo, a design methodology in which distributed designers develop different aspects of the overall system, in a concurrent but controlled way. Our generic mathematical model of contract supports this style of development. This is achieved by focusing on behaviors, by supporting the notion of ldquorich componentrdquo where functional and non-functional aspects of the system can be considered and combined, by representing rich components via their set of associated contracts, and by formalizing the process of component composition.

We study the implementation of a synchronous program as a set of multiple tasks running on the same computer, and scheduled by a real-time operating system using some preemptive scheduling policy, such as fixed priority or earliest-deadline first. Multitask implementations are necessary, for instance, in multiperiodic applications, when the worst-case execution time of the program is larger than its smallest period. In this case, a single-task implementation violates the schedulability assumption and, therefore, the synchrony hypothesis does not hold. We are aiming at semantics-preserving implementations, where, for a given input sequence, the output sequence produced by the implementation is the same as that produced by the original synchronous program, and this under all possible executions of the implementation. Straightforward implementation techniques are not semantics-preserving. We present an intertask communication protocol, called DBP, that is semantics-preserving and memory-optimal. DBP guarantees semantical preservation under all possible triggering patterns of the synchronous program: thus, it is applicable not only to time-, but also event-triggered applications. DBP works under both fixed priority and earliest-deadline first scheduling. DBP is a nonblocking protocol based on the use of intermediate buffers and manipulations of write-to/read-from pointers to these buffers: these manipulations happen upon arrivals, rather than executions of tasks, which is a distinguishing feature of DBP. DBP is memory-optimal in the sense that it uses as few buffers as needed, for any given triggering pattern. In the worst case, DBP requires, at most, N + 2 buffers for each writer, where N is the number of readers for this writer.

The work described in this thesis is done in the context of a long term effort at VERIMAG laboratory to build a complete model based tool-chain for the design and implementation of embedded systems. We follow a layered approach that distinguishes the application level from the architectural/implementation level. The application is described in a high-level language that is independent of implementation details. The application is then mapped to a specified architecture using a number of techniques so that the desired properties of the high level description are preserved. In this thesis, the application is described in Simulink/Stateflow, a wide-spread modeling language that has become a de-facto standard in many industrial domains, such as automotive. At the architectural level we consider single-processor, multi-tasking software implementations. Multi-tasking means that the application software is divided into a number of processes that are scheduled by a real-time operating system, according to some preemptive scheduling policy, such as static-priority or earliest deadline first. Between these two layers we add an intermediate representation layer, based on the synchronous language Lustre, developed at VERIMAG for the last 25 years. This intermediate layer permits us to take advantage of a number of tools developed for Lustre, such as simulators, model-checkers, test generators and code generators. In a first part of the thesis, we study how to translate automatically Simulink/Stateflow models into Lustre. For Simulink this is mostly straightforward, however it still requires sophisticated algorithms for the inference of type and timing information. The translation of Stateflow is much harder for a number of reasons; first Stateflow presents a number of semantically ``unsafe'' features, including non-termination of a synchronous cycle or dependence of semantics on the graphical layout. Second, Stateflow is an automata-based, imperative language, whereas Lustre is a dataflow language. For the first set of problems we propose a number of statically verifiable conditions that define a ``safe'' subset of stateflow. For the second set of problems we propose a set of techniques to encode automata and sequential code into dataflow equations. In the second part of the thesis, we study the problem of implementing synchronous designs in the single-processor multi-tasking architecture described above. The crucial issue is how to implement inter-task communication so that the semantics of the synchronous design are preserved. Standard implementations, using single buffers protected by semaphores to ensure atomicity, or other, lock-free, protocols proposed in the literature do not preserve the synchronous semantics. We propose a new buffering scheme that preserves the synchronous semantics and is also lock-free. We also show that this scheme is optimal in terms of buffer usage.

Recently, we have proposed a set of buffering schemes to preserve the semantics of a synchronous program when the latter is implemented as a set of multiple tasks running under preemptive scheduling. These schemes, however, are not optimal in terms of memory (buffer usage). In this paper we propose a new protocol which generalizes the previous schemes. The new protocol is not only semantics-preserving but also memory-optimal in two senses: first, in terms of the number of buffers required to preserve semantics in the worst case (i.e.,for the "worst" possible arrival/execution pattern of the tasks); second, in terms of the number of buffers required to preserve semantics for any arrival/execution pattern and at any time, assuming no knowledge of future arrivals.

In previous work, we have proposed a method of preserving the functional semantics of model-based designs by the use of static checks and a double-buffer protocol [12]. However, this is restricted to static, fixed-priority scheduling and for high-priority to low-priority communications requires a double buffer to be stored for each pair of communicating tasks. In this paper we extend the method to dynamic-priority scheduling in the form of earliest-deadline-first (EDF) scheduling and show that, although scheduling is dynamic, a static buffering scheme can still be used. We also suggest some memory optimizations of our protocol which still preserve the original functional semantics. Finally, we show how model checking can be used to prove correctness of the scheme.

The Simulink/Stateflow toolset is an integrated suite enabling model-based design and has become popular in the automotive and aeronautics industries. We have previously developed a translator called Simtolus from Simulink to the synchronous language Lustre and we build upon that work by encompassing Stateflow as well. Stateflow is problematical for synchronous languages because of its unbounded behaviour so we propose analysis techniques to define a subset of Stateflow for which we can define a synchronous semantics. We go further and define a "safe" subset of Stateflow which elides features which are potential sources of errors in Stateflow designs. We give an informal presentation of the Stateflow to Lustre translation process and show how our model-checking tool Lesar can be used to verify some of the semantical checks we have proposed. Finally, we present a small case-study.

We present a layered end-to-end approach for the design and implementation of embedded software on a distributed platform. The approach comprises a high-level modeling and simulation layer (Simulink), a middle-level programming and validation layer (SCADE/Lustre) and a low-level execution layer (TTA). We provide algorithms and tools to pass from one layer to the next. First, a translator from Simulink to Lustre. Second, a set of real-time and code-distribution extensions to Lustre. Third, implementation techniques for decomposing a Lustre program into tasks and messages, scheduling the tasks and messages on the processors and the bus, distributing the Lustre code on the execution platform, and generating the necessary "glue" code.

We present a layered end-to-end approach for the design and implementation of embedded software on a distributed platform. The approach comprises a high-level modeling and simulation layer (Simulink), a middle-level programming and validation layer (SCADE/Lustre) and a low-level execution layer (TTA). We provide algorithms and tools to pass from one layer to the next. First, a translator from Simulink to Lustre. Second, a set of real-time and code-distribution extensions to Lustre. Third, implementation techniques for decomposing a Lustre program into tasks and messages, scheduling the tasks and messages on the processors and the bus, distributing the Lustre code on the execution platform, and generating the necessary "glue" code.

We present a method of translating discrete-time Simulink models to Lustre programs. Our method consists of three steps: type inference, clock inference and hierarchical bottom-up translation. In the process, we formalise typing and timing mechanisms of Simulink. The method has been implemented in a prototype tool called S2L. The tool has been used to translate part of an industrial automotive controller provided by Audi.