For the development of high tech industrial systems many different formalisms and tools are required. To ensure consistency of results across different models and tools, tool-integration and model reuse is essential. The main purpose of the Compositional Interchange Format (CIF) is to establish inter-operability of a wide range of tools, including tools for verification and control system design, by means of model transformations to and from CIF. In addition, tools that operate directly on CIF models are available for hybrid system simulation and for supervisory control synthesis.

The presentation discusses how CIF combines a user-friendly modeling language (textual and graphical) with a formal semantics based on a process algebra of automata, where each concept is defined by means of an operator. An overview of the work on CIF in several European projects is given, and different industrial applications are discussed.

Systems and Networks on Chips (NoCs) are a prime design focus of many embedded hardware manufacturers. In addition to functional verification, which is a difficult necessity, the chip designers are facing extremely demanding performance prediction challenges, such as the need to estimate the latency of memory accesses over the NoC.

This talk discusses this problem in the setting of designing globally asynchronous, locally synchronous systems (GALS). In this context, the current state of perfomance prediction practice does either start off from a purely asynchronous modelling hypothesis, and then incorporates restricted synchronicity features, or proceeds in the reverse way, taking synchronicity as the prinicipal modelling hypothesis, that is then weakened to incorporate some form of asynchronicity.

After reviewiewing these principal approaches, we describe foundations and applications of a combination of compositional modeling, model checking, and Markov process theory, to arrive at a viable approach to compute performance quantities directly on industrial, functionally verified GALS models.

The pi-calculus is a very expressive specification language for concurrent programming, but the difficulties in its distributed implementation challenge its candidature to be a canonical model of distributed computation. The mixed choice construct of the pi-calculus, in fact, requires solving a problem of distributed agreement.

The asynchronous pi-calculus, on the other hand, is more suitable for a distributed implementation, but it is rather weak for solving distributed problems. We discuss this expressiveness gap and a related separation between the pi-calculus and CCS.

In order to increase the expressive power of the asynchronous pi-calculus while retaining the suitability for a distributed implementation, we propose a probabilistic extension based on the probabilistic automata of Segala and Lynch. The characteristic of this model is that it distinguishes between probabilistic and nondeterministic behavior. The first is associated with the random choices of the process, while the second is related to the arbitrary decisions of an external scheduler. This separation allows us to reason about adverse scheduling conditions.

We show that the pi-calculus can be encoded in the asynchronous pi-calculus is a compositional and fully distributed way, preserving a notion of (probabilistic) testing semantics.

We present a component-based modeling approach to system-software co-engineering of embedded systems. Our approach is centered around the standardized AADL (Architecture Analysis and Design Language) modeling approach. We formalize a significant subset of AADL, incorporating its recent Error Model Annex for modeling faults and repairs. The major distinguishing aspects of this component-based approach are the possibility to describe nominal hardware and software operations, hybrid (and timing) aspects, as well as probabilistic faults and their propagation and recovery. Moreover, it supports dynamic (i.e., on-the-fly) reconfiguration of components and port connections. The operational semantics gives a precise interpretation to model specifications by providing a mapping onto networks of event-data automata. These networks are then subject to different kinds of formal analysis such as model checking, safety and dependability analysis, and performance evaluation.