Behavioural Specification for Hierarchical Object Composition
- Behavioural specification based on hidden (sorted) algebra constitutes
one of the most promising recently developed formal specification and
verification paradigms for system development.
Here we formally introduce novel concepts of
behavioural object and equivalence between behavioural objects
within the hidden algebra framework.
We formally define several object composition operators on behavioural
objects corresponding to the hierarchical object composition
methodology introduced by CafeOBJ.
We study their basic semantical properties and show that our most
general form of behavioural object composition with synchronisation
has final semantics and a composability property of
behavioural equivalence supporting a high reusability of
verifications.
We also show the commutativity and the associativity of parallel
compositions without synchronisation.
back to Selected Publications