PADVES is associated with CAV 2009


Embedded systems are of steadily growing importance in our everyday lives. Building embedded systems is a multidisciplinary field, requiring skills from different domains. In this workshop, we want to address the challenges arising from the interactions between following issues: verification & validation of non functional requirements, design paradigms, design flow and tool integration:

1. 20 years ago, the first CAV conference was held in Grenoble to emphasize the importance of automatic verification techniques, as opposed to the mostly proof-based and interactive approaches proposed at that time by the formal methods community. Since then, powerful automatic techniques have been developed and proved their applicability. The first success story was obtained in the context of hardware verification, and later, with the help of dedicated models, analysis of timing and non functional properties was made possible, and finally automated abstraction, abstract interpretation and compositional approaches, made possible software verification, in particular in the context of embedded and safety critical systems
   where the demand for verification is high, and the adhesion to restrictive design paradigms is generally accepted. Much ongoing effort concerns dynamic systems.
2. Scalability of verification techniques has received quite some attention from the verification community, but is still an issue, and this will probably always remain so. This is a motivation for a number of proposals of design paradigms achieving some kind of “correctness by construction”, where each framework defines its own notion of correctness. A well-studied paradigm in the context of embedded systems is represented by a number of synchronous languages and their use in the actual development flows for safety critical embedded systems.
   But there are many other application domains calling for other paradigms, allowing a better usage of the available resources.
3. Finally, integration of validation in the design cycle has received much less attention from the verification community. On the other hand, the software engineering community has developed in parallel modelling frameworks such as UML and corresponding transformation frameworks with the aim to facilitate the creation and manipulation of models; this community has coined terms such as Model-Driven Engineering. Much effort has been spent to provide standards and tools allowing to represent and to relate the different models needed in the design process; and finally to produce simulation code or productive code.

Important research challenges have been neglected by the individual research communities. The aim of this workshop is discussing those of interest for the verification community.

Réalisation Axome - Création de sites Internet