In this study, we propose a formal semantics for Basic LOTOS Language Of Temporal Ordering Specification). This is the subset of LOTOS where processes interact with each other by pure synchronizations, without exchanging values. In basic LOTOS we can appreciate the expressiveness of all the LOTOS process constructors (operators) without being distracted by interprocess value communication. LOTOS is an FDT generally applicable to distributed, concurrent information processing systems. During the last decade, a lot of works have been devoted to compilation and verification of LOTOS specifications. While using extended Petri net s as tool for compile a subset of LOTOS has already been pointed out. In this article we propose to extensively make use of a specific kind of high level Petri net s: the M-nets. Such nets, allowing for compositionality, appear particularly well-suited to give a formal semantics for basic LOTOS.
展开▼
