QEST and FORMATS Keynote Speaker

Moshe Vardi

Title: Compositional Temporal Synthesis

Abstract: Synthesis is the automated construction of a system from its specification. In standard temporal-synthesis algorithms, it is assumed the system is constructed from scratch rather than composed from reusable components. This, of course, rarely happens in real life. In real life, almost every non-trivial system, either in hardware or in software, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration and choreography, can also be modeled as synthesis of a system from a library of components. In this talk we describe and study the problem of compositional temporal synthesis, in which we synthesize systems from libraries of reusable components. We define two notions of composition: data-flow composition, which we show is undecidable, and control-flow composition, which we show is decidable. We then explore a variation of control-flow compositional synthesis, in which we construct reliable systems from libraries of unreliable components. Joint work with Yoad Lustig and Sumit Nain.

FORMATS Invited Speakers

Twan Basten

Title: Model-Driven Design-Space Exploration for Software-Intensive Embedded Systems

Abstract: The complexity of today's embedded systems is increasing rapidly. Ever more functionality is realized in software, for reasons of cost and flexibility. This leads to many implementation options that vary in functionality, performance, hardware, etc. Systematic development support during the early phases of design is needed to cope with this complexity. Model-driven development bridges the gap between ad-hoc back-of-the-envelope or spreadsheet calculations and physical prototypes. Models provide insight in the performance characteristics of potential implementation options and are a good means for communication. They ultimately lead to shorter, more predictable development times and better controlled product quality.

The Octopus tool set for model-driven design-space exploration (DSE) supports designers in modeling and analyzing implementation options for embedded software and hardware. Modeling follows the Y-chart paradigm, which advocates a separation between application software functionality, platform implementation choices, and the mapping of software functionality onto the platform. The tool set is centered around DSEIR, the DSE intermediate representation. DSEIR is specifically designed for DSE, separating the concerns of modeling design alternatives, analyzing these alternatives, searching the design space, and diagnosing the results. This organization allows domain-specific modeling in combination with generic analysis techniques such as model checking with Uppaal and simulation with CPN Tools, while safeguarding model consistency and supporting model re-use. The tool set enables fast and accurate exploration of design alternatives for software-intensive embedded systems.

The presentation explains the philosophy behind the Octopus tool set and its architecture and implementation. Model transformations and case studies will be highlighted. The tool set is illustrated in a live demonstration.

---

Kim G. Larsen

Title: Statistical Model Checking, Refinement Checking, Optimization, ... for Stochastic Hybrid Automata

Abstract: Statistical Model Checking (SMC) is an approach that has recently been proposed as new scalable, validation technique for large-scale, complex systems. The core idea of SMC is to conduct some simulations of the system, monitor them, and then use statistical methods in order to decide with some degree of confidence whether the system satisfies the property or not. Based on a natural stochastic semantics of priced timed automata, the tool UPPAAL has in previous work been extended with a new statistical model checking engine.

In this talk we will report on the most recent developments and applications of this SMC branch of UPPAAL. This includes extension to stochastic hybrid auotmata and weighted metric temporal logic. Also, we contemplate on how other branches of UPPAAL may benifit from the new scalabe engine in order to improve their performance as well as scope in terms of models that are suppported, e.g.: efficient generation of counter examples, refinement checking and multi-objective optimization.

Important Dates

Program Committee

Steering Committee

Past Conferences