From Petri Nets with Shared Variables to ITL
| Autor: | Maciej Koutny, Hanna Klaudel, Ben C. Moszkowski |
|---|---|
| Přispěvatelé: | Informatique, Biologie Intégrative et Systèmes Complexes (IBISC), Université d'Évry-Val-d'Essonne (UEVE), School of Computer Science, University of Northumbria at Newcastle [United Kingdom] |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Theoretical computer science
Correctness Computer science Interval temporal logic Concurrency Petri nets 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences relations between models [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] 0202 electrical engineering electronic engineering information engineering Concurrent computing concurrency Programming language Petri net Process architecture behavioural consistency Rotation formalisms in three dimensions 010201 computation theory & mathematics Systems design 020201 artificial intelligence & image processing ITL computer compositional translation |
| Zdroj: | 16th International Conference on Application of Concurrency to System Design (ACSD 2016) 16th International Conference on Application of Concurrency to System Design (ACSD 2016), Jun 2016, Torun, Poland. pp.11--18, ⟨10.1109/ACSD.2016.12⟩ ACSD |
| Popis: | International audience; Petri nets and Interval Temporal Logic (ITL) are two formalisms for the specification and analysis of concurrent computing systems. Petri nets allow for a direct expression of causality aspects in system behaviour and in particular support system verification based on partial order reductions or invariant-based techniques. ITL' on the other hand' supports system verification by proving that the formula describing a system implies the formula describing a correctness requirement. It would therefore be desirable to establish a strong semantical link between these two models' thus allowing one to apply diverse analytical methods and techniques to a given system design. We have recently proposed such a semantical link between the propositional version of ITL (PITL) and Box Algebra (BA)' which is a compositional model of basic (low-level) Petri nets supporting handshake action synchronisation between concurrent processes. In this paper' we extend this result by considering a compositional model of (high-level) Petri nets where concurrent processes communicate through shared variables. The main result is a method for translating a design expressed using a high-level Petri net into a semantically equivalent ITL formula. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|