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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 3/2020

03.01.2020 | Regular Paper

Transitive-closure-based model checking (TCMC) in Alloy

verfasst von: Sabria Farheen, Nancy A. Day, Amirhossein Vakili, Ali Abbassi

Erschienen in: Software and Systems Modeling | Ausgabe 3/2020

Einloggen

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

search-config
loading …

Abstract

We present transitive-closure-based model checking (TCMC): a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive closure (FOLTC). TCMC is an expression of the complete model checking problem for CTLFC as a set of constraints in FOLTC without induction, iteration, or invariants. We implement TCMC in the Alloy Analyzer, showing how a transition system can be expressed declaratively and concisely in the Alloy language. Since the total state space is rarely representable due to the state-space explosion problem, we present scoped TCMC where the property is checked for state spaces of a size smaller than the total state space. We address the problem of spurious instances and carefully describe the meaning of results from scoped TCMC with respect to the complete model checking problem. Using case studies, we demonstrate scoped TCMC and compare it with bounded model checking, highlighting how TCMC can check infinite paths.
Vorheriger Artikel Systematic review of matching techniques used in model-driven methodologies
Nächster Artikel Ark: a constraint-based method for architectural synthesis of smart systems

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 "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

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
Fußnoten
1
This translation increases the size of a transition system.
 
3
A full subgraph of a graph is a subset of the nodes with all edges between these nodes that are found in the original graph.
 
4
Infinite liveness, also described in this figure, is explained in a later subsection.
 
5
The use of id[X] in EG (from which AF and AU are derived) in the TCMC implementation in Fig. 2 requires there to be a looping path from a state back to itself to make an infinite path.
 
6
Existential TCMC requires the satisfying TS instance to have some path from all initial states of the TS instance; however, unless the model requires there to be multiple initial states, usually there is a TS instance with only one initial state meaning there is some path from some initial state.
 
Literatur
1.
Abrial, J.R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRef
2.
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Chechik, M. (ed.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 193–207. Springer, Berlin (1999)
3.
Börger, E.: The ASM method for system design and analysis. A tutorial introduction. In: Frontiers of Combining Systems, Lecture Notes in Computer Science, vol. 3717, pp. 264–283. Springer (2005)
4.
Bradley, A.R.: SAT-based model checking without unrolling. In: International Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 6538, pp. 70–87. Springer (2011)
5.
Chang, F.S.H., Jackson, D.: Symbolic model checking of declarative relational models. In: International Conference on Software Engineering, pp. 312–320. ACM (2006)
6.
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Computer Aided Verification, Lecture Notes In Computer Science, vol. 2404, pp. 241–268. Springer (2002)
7.
Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Boca Raton (1999)MATH
8.
Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Form. Methods Syst. Design 10, 47–71 (1997)CrossRef
9.
Cunha, A.: Bounded model checking of temporal formulas with Alloy. In: International Conference on Abstract State Machines. Alloy, B, VDM, and Z, pp. 303–308. Springer, Berlin (2014)
10.
Del Castillo, G., Winter, K.: Model checking support for the ASM high-level language. In: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes In Computer Science, vol. 1785, pp. 331–346. Springer (2000)
11.
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRef
12.
Dold, A.: A formal representation of abstract state machines using PVS. Verifix Technical Report Ulm/6.2, Universität Ulm (1998)
13.
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol. 2919, pp. 333–336. Springer (2004)
14.
Farheen, S.: Improvements to transitive-closure-based model checking in Alloy. M.Math thesis, University of Waterloo, David R. Cheriton School of Computer Science (2018)
15.
Frias, M.F., Galeotti, J.P., López Pombo, C.G., Aguirre, N.M.: DynAlloy: upgrading Alloy with actions. In: International Conference on Software Engineering, pp. 442–451. ACM (2005)
16.
Grumberg, O., Long, D.E.: Model checking and modular verification. In: Proccedings of 2nd International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 527, pp. 250–265. Springer (1991)
17.
Immerman, N., Vardi, M.: Model checking and transitive-closure logic. In: Computer-Aided Verification, Lecture Notes in Computer Science, vol. 1254, pp. 291–302. Springer (1997)
18.
International Organisation for Standardization. Information Technology Z Formal Specification Notation Syntax, Type System and Semantics (2000)
19.
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRef
20.
Jackson, D.: Software Abstractions—Logic, Language, and Analysis. MIT Press, Cambridge (2012)
21.
Kember, M., Tran, L., Gao, G., Day, N.A.: Extracting counterexamples from transitive-closure-based model checking. In: Workshop on Modelling in Software Engineering (MISE)@ International Conference on Software Engineering (ICSE), pp. 47–54. ACM (2019)
22.
Krings, S., Leuschel, M.: Proof assisted bounded and unbounded symbolic model checking of software and system models. Sci. Comput. Program. 15, 41–63 (2018)CrossRef
23.
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10, 185–203 (2008)CrossRef
24.
Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: Foundations of Software Engineering, pp. 373–383. ACM (2016)
25.
McMillan, K.: Symbolic model checking: an approach to the state explosion problem. Ph.D. thesis, Pittsburgh, PA, USA (1992)
26.
Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering, vol. 1, 609–619. IEEE (2015)
27.
Nissanke, N.: Formal Specification: Techniques and Applications, 1st edn. Springer, Berlin (1999)CrossRef
28.
Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRef
29.
Regis, G., Cornejo, C., Gutiérrez Brida, S., Politano, M., Raverta, F., Ponzio, P., Aguirre, N., Galeotti, J.P., Frias, M.: DynAlloy analyzer: a tool for the specification and analysis of alloy models with dynamic behaviour. In: Foundations of Software Engineering, pp. 969–973. ACM (2017)
30.
Schellhorn, G., Ahrendt, W.: Reasoning about abstract state machines: the WAM case study. J. Univers. Comput. Sci. 3(4), 377–413 (1997)MathSciNetMATH
31.
Selic, B.: From model-driven development to model-driven engineering. In: Euromicro Conference on Real-Time Systems. IEEE Computer Society (2007)
32.
Serna, J., Day, N.A., Farheen, S.: DASH: a new language for declarative behavioural requirements with control state hierarchy. In: International workshop on model-driven requirements engineering (MoDRE)@ IEEE international requirements engineering conference (RE), pp. 64–68 (2017)
33.
Vakili, A.: Temporal logic model checking as automated theorem proving. Ph.D. thesis, University of Waterloo, David R. Cheriton School of Computer Science (2016)
34.
Vakili, A., Day, N.A.: Temporal model checking in alloy. In: International Conference on Abstract State Machines, Alloy, B, VDM, and Z, Lecture Notes In Computer Science, vol. 7316, pp. 150–163. Springer (2012)
35.
36.
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 54–66. Springer (1999)
Metadaten
Titel
Transitive-closure-based model checking (TCMC) in Alloy
verfasst von
Sabria Farheen
Nancy A. Day
Amirhossein Vakili
Ali Abbassi
Publikationsdatum
03.01.2020
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 3/2020
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-019-00763-8

Weitere Artikel der Ausgabe 3/2020

Software and Systems Modeling 3/2020 Zur Ausgabe

Special Section Paper

From analytical purposes to data visualizations: a decision process guided by a conceptual framework and eye tracking

Guest Editorial

Special section of BPMDS’2017: enabling business transformation by business process modeling, development and support

Regular Paper

Systematic review of matching techniques used in model-driven methodologies

Theme Section Paper

Towards high-level fuzzy control specifications for building automation systems

Guest Editorial

Editorial to the theme section on model-based engineering of smart systems

Regular Paper

Benchmarking bidirectional transformations: theory, implementation, application, and assessment