Observational refinement and merge for disjunctive MTSs
File(s)paper.pdf (339.22 KB)
Accepted version
Author(s)
Ben-David, S
Chechik, M
Uchitel, S
Type
Conference Paper
Abstract
Modal Transition System (MTS) is a well studied formal- ism for partial model specification. It allows a modeller to distinguish between required, prohibited and possible transitions. Disjunctive MTS (DMTS) is an extension of MTS that has been getting attention in re- cent years. A key concept for (D)MTS is refinement , supporting a devel- opment process where abstract specifications are gradually refined into more concrete ones. Refinement comes in different flavours: strong , ob- servational (where τ -labelled transitions are taken into account), and alphabet (allowing the comparison of models defined on different alpha- bets). Another important operation on (D)MTS is that of merge : given two models M and N , their merge is a model P which refines both M and N , and which is the least refined one. In this paper, we fill several missing parts in the theory of DMTS refine- ment and merge. First and foremost, we define observational refinement for DMTS. While an elementary concept, such a definition is missing from the literature to the best of our knowledge. We prove that our defi- nition is sound and that it complies with all relevant definitions from the literature. Based on the new observational refinement for DMTS, we ex- amine the question of DMTS merge, which was defined so far for strong refinement only. We show that observational merge can be achieved as a natural extension of the existing algorithm for strong merge of DMTS. For alphabet merge however, the situation is different. We prove that DMTSs do not have a merge under alphabet refinement.
Editor(s)
Artho, C
Legay, A
Peled, D
Date Issued
2016-09-22
Online Publication Date
2017-09-22T06:00:21Z
Date Acceptance
2016-09-01
ISBN
978-3-319-46519-7
ISSN
0302-9743
Publisher
Springer
Start Page
287
End Page
303
Journal / Book Title
Automated Technology for Verification and Analysis, ATVA 2016
Volume
9938
Copyright Statement
© Springer International Publishing AG 2016. The final publication is available at Springer via https://link.springer.com/chapter/10.1007%2F978-3-319-46520-3_19
Source Database
web-of-science
Identifier
http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000389808100019&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=1ba7043ffcc86c417c072aa74d649202
Source
14th International Symposium on Automated Technology for Verification and Analysis (ATVA)
Subjects
Science & Technology
Technology
Automation & Control Systems
Computer Science, Artificial Intelligence
Computer Science, Theory & Methods
Computer Science
MODAL TRANSITION-SYSTEMS
08 Information And Computing Sciences
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2016-10-17
Finish Date
2016-10-20
Country
Chiba, JAPAN