Observational re- finement and merge for disjunctive mtss.

MARSHA CHECHIK; SEBASTIAN UCHITEL; SHOHAM BEN DAVID

Conferencia; 14th International Symposium on Automated Technology for Verification and Analysis; 2016

Modal Transition Systems (MTS) are a well studied formalism for partial model specification, allowing a modeller to distinguish between required, prohibited and possible transitions. An MTS describes a set of possible implementations. Disjunctive MTS (DMTS) is an extension of MTS that has been attracting attention in recent years. A key concept for (D)MTSs is that of refinement, supporting a development process where abstract specifications are gradually refined into more concrete ones. Refinement comes in different flavours: strong, observational, and alphabet. Each refinement type can be either modal, where a refinement relation is syntactically defined on the two models, or thorough, where the sets of implementations are compared. The first contribution of this paper is the definition of modal observational refinement for DMTS. Although a crucial concept, it is, to the best of our knowledge, missing from the literature. We prove that our definition is sound and that it complies with other refinement definitions in the literature.Our second contribution deals with the operation of (D)MTS merge: given two models M and N, find a common refinement of them that is the least refined one. MTS are not closed under merge for any refinement type. DMTS were shown to be closed for merge under strong refinement and not closed under thorough alphabet refinement. Using our new observational refinement definition, we show that DMTS are closed for observational refinement and not closed for modal alphabet refinement.