Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Observational Refinement and Merge for Disjunctive MTSs

verfasst von : Shoham Ben-David, Marsha Chechik, Sebastian Uchitel

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Modal Transition System (MTS) is a well studied formalism 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 recent years. A key concept for (D)MTS is refinement, supporting a development process where abstract specifications are gradually refined into more concrete ones. Refinement comes in different flavours: strong, observational (where \(\tau \)-labelled transitions are taken into account), and alphabet (allowing the comparison of models defined on different alphabets). 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 refinement 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 definition is sound and that it complies with all relevant definitions from the literature. Based on the new observational refinement for DMTS, we examine 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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Synthesizing Skeletons for Reactive Systems
Nächstes Kapitel Equivalence-Based Abstraction Refinement for HORS Model Checking
Literatur
1.
Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: Complexity of decision problems for mixed and modal specifications. In: FoSSaCS, pp. 112–126 (2008)
2.
Antonik, A., Michael, H., Larsen, K.G., Nyman, U., Wasowski, A.: Exptime-complete decision problems for modal and mixed specifications. Electr. Notes Theor. Comput. Sci. 242(1), 19–33 (2009)MathSciNetCrossRefMATH
3.
Ben-David, S., Chechik, M., Uchitel, S.: Merging partial behaviour models with different vocabularies. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 91–105. Springer, Heidelberg (2013)CrossRef
4.
Beneš, N., Černá, I., Křetínský, J.: Modal transition systems: composition and LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 228–242. Springer, Heidelberg (2011)CrossRef
5.
Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275–289. Springer, Heidelberg (2011)CrossRef
6.
Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 112–126. Springer, Heidelberg (2009)CrossRef
7.
Fahrenberg, U., Legay, A., Traonouez, L.-M.: Structural refinement for the modal nu-calculus. In: Ciobanu, G., Méry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 169–187. Springer, Heidelberg (2014)
8.
Fantechi, A., Gnesi, S.: Formal modeling for product families engineering. In: SPLC, pp. 193–202 (2008)
9.
Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with a one-selecting variant. J. Logic Algebraic Program. 77(1–2), 20–39 (2008)MathSciNetCrossRefMATH
10.
Fischbein, D.: Foundations for behavioural model elaboration using modal transition systems. Ph.D. thesis, Imperial College London (2012)
11.
Fischbein, D., Braberman, V., Uchitel, S.: A sound observational semantics for modal transition systems. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 215–230. Springer, Heidelberg (2009)CrossRef
12.
Fischbein, D., D’Ippolito, N., Brunet, G., Chechik, M., Uchitel, S.: Weak alphabet merging of partial behavior models. ACM Trans. Softw. Eng. Methodol. (TOSEM) 21(2), 9 (2012)CrossRef
13.
Fischbein, D., Uchitel, S.: On correct and complete strong merging of partial behaviour models. In: SIGSOFT FSE, pp. 297–307 (2008)
14.
Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Proceedings of Logic at Botik, Symposium on Logical Foundations of Computer Science, Pereslav-Zalessky, USSR, pp. 163–180 (1989)
15.
16.
Larsen, K.G., Nyman, U., Wąsowski, A.: On modal refinement and consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105–119. Springer, Heidelberg (2007)CrossRef
17.
Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210 (1988)
18.
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108–117 (1990)
19.
Lüttgen, G., Vogler, W.: Modal interface automata. Logical Methods Comput. Sci. 9(3) (2013)
20.
Uchitel, S., Chechik, M.: Merging partial behavioural models. In: SIGSOFT FSE, pp. 43–52 (2004)
Metadaten
Titel
Observational Refinement and Merge for Disjunctive MTSs
verfasst von
Shoham Ben-David
Marsha Chechik
Sebastian Uchitel
Copyright-Jahr
2016
Buch
Automated Technology for Verification and Analysis

Print ISBN: 978-3-319-46519-7

Electronic ISBN: 978-3-319-46520-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46520-3_19

Premium Partner

    Bildnachweise