PADVES: Platforms for Analysis, Design and Verification of Embedded Systems

June 27th, 2009       Grenoble, France organised and funded by ARTIST 

Topics addressed


The topics addressed by the workshop are as follows:
  • Even after many years of work on unifying modelling frameworks, it is still the case that for a complex system, different models are built for different purposes. For example, a design model and a model for performance analysis are built by different people, with different tools, and using different paradigms. This means that different aspects of a system are defined by different models corresponding to different “views” of the system. The resulting collection of views should be structured, that is the semantics of each of these views related in order to form a complete specification of the system to be implemented or validated. Central related questions are defining and checking consistency: does the complete specification characterizes at least one valid system? how can this be verified? preferably without computing a global model, and how that consistency is preserved by the design cycle operations, such as refinement or composition?
    In addition, due to the heterogeneous nature of embedded systems, in the sense that they involve mechanical/hardware/software parts, different modeling paradigms and tools are used for modelling different parts of the system, as different paradigms are well adapted or accepted by the respective user community. Also here, the challenge is reasoning on the composition of models of heterogeneous nature using either different tools or a tool offering the capability to unify very different paradigms without too much loss of abstraction.
  • A related challenge is how reconcile early – speculative - validation of non functional, platform related properties without imposing unnecessary partition constraints which turn out to be badly chosen at later design stages.
  • The introduction of new paradigms for designing specific classes of embedded systems and the trend towards adaptive, self-organizing, self-healing, … systems poses new challenges for the verification of embedded systems which in the past has been mainly of static nature
  • The increasing complexity, heterogeneity and ubiquity of embedded systems leads to the emergence of new non functional properties for which appropriate models and verification methods have to be developed. This is partly addressed by the verification community, but the interaction between the design approaches and the verification techniques are rarely studied.
  • Increasingly, embedded systems are conceived as service oriented systems where it should be possible to plug in new functionalities with a reduced effort. This lead to the definition of component concepts which differ from those used in pure functional or object oriented languages. Exploiting such concepts for achieving designs which are both more flexible and easier to verify remains a challenge. In particular such component based systems are “complex” in the sense that the whole system may question properties of its sub components, resulting on the emergence of system properties that could not be deduced by reasoning on each component taken in isolation. This makes classical and well studied modular reasoning difficult. Different notions of contracts have been studied to address this issue.

Therefore, the workshop focuses on the integration of tool supported analysis and validation techniques into a development process in the domain of embedded systems. It is expected that the submitted contribution handle about model-based approaches for the development of embedded systems with respect to the problematic of their validation or tools or case studies on the integration of existing validation methods into design flows used in practice.

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet