TY - JOUR
T1 - A modal specification theory for components with data
AU - S. Bauer, Sebastian
AU - Larsen, Kim Guldstrand
AU - Legay, Axel
AU - Nyman, Ulrik Mathias
AU - Wasowski, Andrzej
PY - 2014
Y1 - 2014
N2 - Modal specification is a well-known formalism used as an abstraction theory for transition 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 refinement 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 theory; that is parallel composition, conjunction and quotient. As MSDs are by nature potentially infinite-state systems, we propose symbolic representations based on effective predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.
AB - Modal specification is a well-known formalism used as an abstraction theory for transition 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 refinement 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 theory; that is parallel composition, conjunction and quotient. As MSDs are by nature potentially infinite-state systems, we propose symbolic representations based on effective predicates. Our theory serves as a new abstraction-based formalism for transition systems with data.
KW - Modal transition systems
KW - Specifications
KW - Interfaces
KW - Data abstraction
KW - Modal specifications with data
KW - Modal transition systems
KW - Specifications
KW - Interfaces
KW - Data abstraction
KW - Modal specifications with data
M3 - Journal article
SN - 0167-6423
VL - 83
SP - 106
EP - 128
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -