Because of their complexity, embedded systems are designed with sub-systems or components taken in charge by different development teams or entities and with different modeling frameworks and simulation tools, depending on the characteristics of each component. Unfortunately, this diversity of tools and semantics makes the integration of these heterogeneous components difficult. Thus, to evaluate their integration before their hardware or software is available, one solution would be to merge them into a common modeling framework. Yet, such a holistic environment supporting many computation and computation semantics seems hard to settle. Another solution we investigate in this paper is to generically link their respective simulation environments in order to keep the strength and semantics of each component environment.The paper presents a method to simulate heterogeneous components of embedded systems in real-time. These components can be described at any abstraction level. Our main contribution is a generic glue that can analyze in real-time the state of different simulation environments and accordingly enforce the correct communication semantics between components. Once presented in a generic way, our glue is illustrated with Apache Kafka as the communication facility between simulation engines. It is then applied to two model and simulation frameworks: TTool and SystemC. Finally, Zigbee serves as a case study to illustrate the strengths of our approach.

International audience

International audience

The necessity of handling the increasing complexity of embedded systems has led to the growth of reuse-based design. At the same time, the systems must still satisfy strict requirements on reliability and correctness. This paper proposes a formal analysis of parallel composition of I/O automata. This analysis leads to identification of novel composition rules guaranteeing the correctness-by-construction, and will provide a basis for a sound compositional development of components (Intellectual Property blocks).

International audience

Ensuring the compliance of developed software with general and application-specific security requirements is a challenging task due to the lack of automatic and formal means to lead this verification. In this paper, we present our approach that aims at integrating the formal specification and verification of security guidelines in early stages of the development lifecycle by combining the model checking together with information flow analysis. We present our framework that is based on an extension of LTS (Labeled Transition Systems) by data dependence information to cover the end-to-end specification and verification of security guidelines.

Secure software can be obtained out of two distinct processes: security by design, and security by certification. The former approach has been quite extensively formalized as it builds upon models, which are verified to ensure security properties are attained and from which software is then derived manually or automatically. In contrast, the latter approach has always been quite informal in both specifying security best practices and verifying that the code produced conforms to them. In this paper, we focus on the latter approach and describe how security guidelines might be captured by security experts and verified formally by developers. Our technique relies on abstracting actions in a program based on modularity, and on combining model checking together with information flow analysis. Our goal is to formalize the existing body of knowledge in security best practices using formulas in the MCL language and to conduct formal verifications of the conformance of programs with such security guidelines. We also discuss our first results in creating a methodology for the formalization of security guidelines.

International audience

The increasing complexity of System-on-Chip (SoC) requires a complete reexamination of design and validation methods prior to final implementation whereas faster system design space exploration is today’s requirement to speed up the design process in order to cope with ‘timeto- market’ constraint. We have introduced SoC modeling approach which mixes simulation and formal modeling and verification methods for efficient design space exploration phase of SoC design cycle. The applications are described as a network of communicating tasks whose behaviors are abstracted. Because applications are abstract, it is possible to significantly increase the speed of simulation, to perform a quick performance analysis and apply static formal analysis techniques at higher level of abstraction. The proposed methodology has been employed in the design of a telecommunication system. A part of the application is modeled as a set of tasks in a modeling language and their behavior is monitored as a waveform of events in a simulation environment.