Приглашенные докладчики
Аннотации докладов
Methods and Tools for Rigorous Component-based Design
Joseph Sifakis
System design radically differs from pure software design as it must take into account not only functional but also extra-functional requirements regarding the use of resources of the execution platform such as time, memory and energy. The design flow starts from specifications and leads to an implementation on a given execution platform. It involves the use of methods and tools for progressively deriving the implementation by making adequate design choices.
We advocate for rigorous system design which ensures by construction essential properties of the designed system. A necessary condition for rigorousness is the use of a single semantic model for the languages used to describe the system at different abstraction levels in order to maintain the overall coherency in the design flow. We discuss essential features of such a model including expressiveness, incremental component-based description and constructivity.
We present a rigorous design flow which derives a correct system implementation from
- an application software described as a network of processes communicating by write/read operations on fifo queues;
- a description of a hardware architecture;
- a mapping of the processes into processors of the architecture. The implementation is obtained by successive application of source-to-source transformations that are correct-by-construction; in particular, the derived system descriptions are observationally equivalent to the application software. Furthermore, the transformations are driven by results provided by a performance analysis tool to take into account extra-functional requirements.
The design flow is supported by a set of integrated tools including a compiler, models transformers, a simulator and a performance analysis tool. We present a non trivial case study illustrating the application of the proposed design flow and its use for deriving optimal implementations.
A Connector Algebra for Place-Transition Petri Nets
(FME Invited Lecture)
Ugo Montanari
(Joint work with Roberto Bruni, Pisa, and Hernan Melgratti, Buenos Aires)
In a paper by Roberto Bruni, Ivan Lanese and the speaker, an algebra of stateless connectors was presented. It consists of five kinds of basic connectors (plus their duals), namely symmetry, synchronization, mutual exclusion, hiding and inaction. The connectors can be composed in series or in parallel and the resulting networks are equipped with a normal form axiomatization. These networks are quite expressive: for instance they can model the architectural design language CommUnity by Luis Fiadeiro and, employing in addition a simple 1-state buffer, the coordination language REO by Farhad Arbab et al. In a recent paper, Pawel Sobocinski employed essentially the same steteful extension of connector algebra to compose Condition-Event (C/E) Petri nets and showed a close correspondence of the two semantics. Surprisingly enough, the connector algebra has operations quite different than those of CCS-like process calculi usually employed for making Petri nets compositional, and closer to approaches like REO and tiles, the latter by Fabio Gadducci, Roberto Bruni and the speaker.
In the talk we will present the connector algebra and we will show how to extend Sobocinski approach towards Place Transition nets - where, contrary to Condition-Event systems, places can contain an unbounded number of tokens - thus opening the way towards more expressive connector models.
Petri Net Distributability
Eike Best and Philippe Darondeau (INRIA, IRISA, France)
A Petri net is distributed if, given an allocation of transitions to (geographical) locations, no two transitions at different locations share a common input place. A system is distributable if there is some distributed Petri net implementing it.
This talk addresses the question of which systems can be distributed, while respecting a given allocation. The paper states the problem formally and discusses several examples illuminating the current status of this work.