Bauer, Sebastian S.6; Larsen, Kim G.1; Legay, Axel3; Nyman, Ulrik1; Wasowski, Andrzej7
1 CISS - Center for Embedded Software Systems, The Technical Faculty of IT and Design, Aalborg University, VBN2 Distributed Systems and Semantics, The Technical Faculty of IT and Design, Aalborg University, VBN3 Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University, VBN4 Aalborg U Robotics, The Faculty of Humanities, Aalborg University, VBN5 The Faculty of Engineering and Science (TECH), Aalborg University, VBN6 Institut für Informatik, Ludwig-Maximilians-Universität München7 Department of Electronic Systems, The Technical Faculty of IT and Design, Aalborg University, VBN
Modal specification is a well-known formalism used as an abstraction theory for tran- sition systems. Modal specifications are transition systems equipped with two types of transitions: must-transitions that are mandatory to any implementation, and may- transitions that are optional. The duality of transitions allows for developing a unique approach for both logical and structural compositions, and eases the step-wise refine- ment process for building implementations. We propose Modal Specifications with Data (MSDs), the first modal specification theory with explicit representation of data. Our new theory includes the most commonly seen ingredients of a specification the- ory; that is parallel composition, conjunction and quotient. As MSDs are by nature potentially infinite-state systems, we propose symbolic representations based on effec- tive predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.
Science of Computer Programming, 2014, Vol 83, p. 106-128
Modal Transition Systems, Specifications, Interfaces, Data Abstraction, Modal Specifications with Data