[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Call for contributions: PADVES associated with CAV 2009



--------------------------------------------------------------------
                     Call for contributions
--------------------------------------------------------------------

                           PADVES'09
                          Workshop on
   Platforms for Analysis, Design and Verification of Embedded Systems

                     Colocated with CAV'09

                Grenoble (France), June 27, 2009

          http://www.artist-embedded.org/artist/PADVES.html

--------------------------------------------------------------------

FORMAT of the WORKSHOP
----------------------
This workshop will consist partly of invited high level presentations with
following discussion sessions.

We sollicitate submissions of a similar form which are not necessarily expected
to be non published results, but which are meaningful for a discussion on the
topics of the workshop.

The presentations will be selected from abstract of a few pages to be sent by
email to one of the organizers.


CONTRIBUTIONS and IMPORTANT DATES
---------------------------------
Important Dates and paper submission
Abstract submission 	             May 30, 2009
Notification of acceptance 	    June 10, 2009
Workshop Date 	                    June 27, 2009


MOTIVATIONS and TOPICS
------

    * 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.

We consider a spectrum of topics related to the design of platforms for building
functionally correct embedded and complex systems with guaranteed properties.

     * Paradigms for designing specific classes of embedded systems and
challenges for verifying non functional and platform related characteristics
     * Validation of complex architectures and system level analysis. This
includes handling heterogeneity and multi-views from design to validation or
verification.
     * Representations for systems, their platforms and their properties
allowing their efficient exploitation by validation and code generation tools
     * Platforms for integrating validation and development: challenges and
solutions
     * Solutions for tool integration
     * Adapting validation techniques to the type of functional/non functional
properties under study
     * Studying emergence of properties in complex embedded systems


INVITED SPEAKERS

to be announced shortly


ORGANISERS
     * Kim Larsen (CISS, Aalborg University)
     * Christophe Gaston (CE-LIST, Sacley)
     * Susanne Graf (VERIMAG/CNRS)