(TP)I, (Timed/Probabilistic) Interfaces

Several industrial sectors involving complex embedded systems have recently experienced deep changes in their organization, aerospace and automotive being the most prominent examples. In the past, they were organized around vertically integrated companies, supporting in-house design activities from specification to implementation. Nowadays, systems are tremendously big and complex, and it is almost impossible for one single team to have the complete control of the entire chain of design from the specification to the implementation. In fact, complex systems now result from the assembling of several components. These many components are in general designed by teams, working independently but with a common agreement on what the interface of each component should be. Such an interface precises the behaviors expected from the component as well as the environment in where it can be used. The main advantage is that it does not impose any constraint on the way the component is implemented, hence allowing for independent implementation. According to state of practice, interfaces are typically described using Word/Excel text documents or modeling languages such as UML/XML. We instead recommend relying most possibly on mathematically sound formalisms, thus best reducing ambiguities. We propose to study mathematical formalisms for interface theories with all the operators needed to reason on them in a proper way, i.e., composition, refinement, quotient, and dissimilar alphabets. We will also focus on implementation (integration in UPPAAL and INTERSMV toolsets) and efficient algorithms. Our results will be extended to timed and stochastic systems. Finally, we will also consider concurrency and modular verification.