Abstract
Modal transition systems are an elegant way to formalise the design process of a system through refinement and composition. Here we propose to adapt this methodology to asynchronous composition via Petri nets. The Petri nets that we consider have distinguished labels for inputs, outputs, internal communications and silent actions and "must" and "may" modalities for transitions. The input/output labels show the interaction capabilities of a net to the outside used to build larger nets by asynchronous composition via communication channels. The modalities express constraints for Petri net refinement taking into account observational abstraction from silent transitions. Modal I/O-Petri nets are equipped with a modal transition system semantics. We show that refinement is preserved by asynchronous composition and by hiding of communication channels. We study compatibility properties which express communication requirements for composed systems and we show that these properties are decidable, they are preserved in larger contexts and also by modal refinement. On this basis we propose a methodology for the specification of distributed systems in terms of modal I/O-Petri nets which supports incremental design, encapsulation of components, stepwise refinement and independent implementability.
Original language | English |
---|---|
Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Number of pages | 16 |
Volume | 8358 LNCS |
Publisher | Springer |
Publication date | 1 Jan 2014 |
Pages | 219-234 |
ISBN (Print) | 9783319051185 |
DOIs | |
Publication status | Published - 1 Jan 2014 |
Event | 8th International Symposium on Trustworthy Global Computing - Buenos Aires, Argentina Duration: 30 Aug 2013 → 31 Aug 2013 Conference number: 8th |
Conference
Conference | 8th International Symposium on Trustworthy Global Computing |
---|---|
Number | 8th |
Country/Territory | Argentina |
City | Buenos Aires |
Period | 30/08/2013 → 31/08/2013 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 8358 LNCS |
ISSN | 0302-9743 |