Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 4/2022

12.09.2022

Pardinus: A Temporal Relational Model Finder

verfasst von: Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen, um Zugang zu erhalten
share
TEILEN

Abstract

This article presents \(\mathsf {Pardinus}\), an extension of the popular \(\mathsf {Kodkod}\) relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. \(\mathsf {Pardinus}\) includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.
Vorheriger Artikel Faster Linear Unification Algorithm
Nächster Artikel From Specification to Testing: Semantics Engineering for Lua 5.2

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Fußnoten
2
In practice, \(\mathsf {Kodkod}\) and \(\mathsf {Pardinus}\) are Java libraries and problems are defined programatically.
 
3
\(\mathsf {Kodkod}\) (and \(\mathsf {Pardinus}\)) also have some limited support for integers which we omit in this presentation.
 
4
The https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09642-2/MediaObjects/10817_2022_9642_Figdo_HTML.gif section is not used as its restricted syntax makes it a complex target for generation from \(\mathsf {Pardinus}\).
 
5
Remark that we use mathematical symbols rather than concrete SMV syntax for better readability. However, future (\({{\,\mathrm{{\mathsf {X}}}\,}}\), \({{\,\mathrm{{\mathsf {G}}}\,}}\), \({{\,\mathrm{{\mathsf {F}}}\,}}\), \(\mathbin {{\mathsf {U}}}\) and \(\mathbin {{\mathsf {R}}}\)) and past (\({{\,\mathrm{{\mathsf {Y}}}\,}}\), \({{\,\mathrm{{\mathsf {H}}}\,}}\), \({{\,\mathrm{{\mathsf {O}}}\,}}\), \(\mathbin {{\mathsf {S}}}\) and \(\mathbin {{\mathsf {T}}}\)) temporal operators follow the standard textual notation also used in \(\mathsf {SMV}\).
 
6
For instance, \(\mathsf {Pardinus}\) also implements an operation to change a segment of a path, which is used by the \(\mathsf {Alloy~6}\) \(\mathsf {Analyzer}\) to change the initial state and for forking paths.
 
7
Although omitted for simplicity, bounding expressions may also refer to concrete atoms as regular constant bounds. These are ignored during symmetry breaking.
 
8
The complete results are available online at https://​bit.​ly/​2YF6hWL, and scripts to reproduce the results available at the \(\mathsf {Pardinus}\) repository.
 
Literatur
1.
Bagheri, H., Malek, S.: Titanium: efficient analysis of evolving Alloy specifications. In: SIGSOFT FSE, pp. 27–38. ACM (2016)
2.
Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: TACAS, LNCS, vol. 2619, pp. 18–33. Springer (2003)
3.
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS, LNCS, vol. 1579, pp. 193–207. Springer (1999)
4.
5.
Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The Electrum Analyzer: model checking relational first-order temporal specifications. In: ASE, pp. 884–887. ACM (2018)
6.
Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: Simulation under arbitrary temporal logic constraints. In: F-IDE@FM, EPTCS, vol. 310, pp. 63–69 (2019)
7.
Castillos, K.C., Waeselynck, H., Wiels, V.: Show me new counterexamples: a path-based approach. In: ICST, pp. 1–10. IEEE (2015)
8.
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: CAV, LNCS, vol. 8559, pp. 334–342. Springer (2014)
9.
10.
Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979) CrossRefMATH
11.
Chang, F.S., Jackson, D.: Symbolic model checking of declarative relational models. In: ICSE, pp. 312–320. ACM (2006)
12.
Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transf. 9(5–6), 429–445 (2007) CrossRefMATH
13.
Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model finding. In: CADE-19 Workshop on Model Computation (2003)
14.
Clarisó, R., Cabot, J.: Diverse scenario exploration in model finders using graph kernels and clustering. In: ABZ, LNCS, vol. 12071. Springer (2020)
15.
Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: KR, pp. 148–159. Morgan Kaufmann (1996)
16.
Cunha, A.: Bounded model checking of temporal formulas with Alloy. In: ABZ, LNCS, vol. 8477, pp. 303–308. Springer (2014)
17.
Cunha, A., Macedo, N., Guimarães, T.: Target oriented relational model finding. In: FASE, LNCS, vol. 8411, pp. 17–31. Springer (2014)
18.
19.
Dominguez, A.L.J., Day, N.A.: Generating Multiple Diverse Counterexamples for an EFSM. Technical Report. CS-2013-06. University of Waterloo (2013)
20.
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: CAV, LNCS, vol. 2725, pp. 27–39. Springer (2003)
21.
Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: upgrading Alloy with actions. In: ICSE, pp. 442–451. ACM (2005)
22.
Ganov, S.R., Khurshid, S., Perry, D.E.: Annotations for Alloy: automated incremental analysis using domain specific solvers. In: ICFEM, LNCS, vol. 7635, pp. 414–429. Springer (2012)
23.
Hölldobler, S., Manthey, N., Nguyen, V.H., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: ICACSIS, pp. 201–206. IEEE (2011)
24.
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997) CrossRef
25.
Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2016)
26.
Kromodimoeljo, S.: Controlling the generation of multiple counterexamples in LTL model checking. PhD Thesis, The University of Queensland (2014)
27.
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994) CrossRef
28.
Lamport, L.: Specifying Systems: The \(\rm TLA^+\) Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)
29.
Leuschel, M., Butler, M.J.: ProB: a model checker for B. In: FME, LNCS, vol. 2805, pp. 855–874. Springer (2003)
30.
Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: SIGSOFT FSE, pp. 373–383. ACM (2016)
31.
Macedo, N., Cunha, A.: Alloy meets \({{\rm TLA}}^{+}\): an exploratory study. CoRR (2016).abs/1603.03599
32.
Macedo, N., Cunha, A., Guimarães, T.: Exploring scenario exploration. In: FASE, LNCS, vol. 9033, pp. 301–315. Springer (2015)
33.
Macedo, N., Cunha, A., Pessoa, E.: Exploiting partial knowledge for efficient model analysis. In: ATVA, LNCS, vol. 10482, pp. 344–362. Springer (2017)
34.
35.
Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: CADE, LNCS, vol. 10395, pp. 148–165. Springer (2017)
36.
Montaghami, V., Rayside, D.: Extending Alloy with partial instances. In: ABZ, LNCS, vol. 7316, pp. 122–135. Springer (2012)
37.
Near, J.P., Jackson, D.: An imperative extension to Alloy. In: ASM, LNCS, vol. 5977, pp. 118–131. Springer (2010)
38.
Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE, pp. 232–241. IEEE (2013)
39.
Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12(1), 9–21 (2010) CrossRef
40.
Ponzio, P., Aguirre, N., Frias, M.F., Visser, W.: Field-exhaustive testing. In: SIGSOFT FSE, pp. 908–919. ACM (2016)
41.
Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: FM, LNCS, vol. 10951, pp. 568–587. Springer (2018)
42.
Reynolds, A., Tinelli, C., Goel, A., Krstic, S.: Finite model finding in SMT. In: CAV, LNCS, vol. 8044, pp. 640–655. Springer (2013)
43.
Rosner, N., Pombo, C.G.L., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F.: Parallel bounded verification of Alloy models by TranScoping. In: VSTTE, LNCS, vol. 8164, pp. 88–107. Springer (2013)
44.
Rosner, N., Siddiqui, J.H., Aguirre, N., Khurshid, S., Frias, M.F.: Ranger: parallel analysis of Alloy models by range partitioning. In: ASE, pp. 147–157. IEEE (2013)
45.
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. STTT 12(2), 123–137 (2010) CrossRef
46.
Saeki, T., Ishikawa, F., Honiden, S.: Automatic generation of potentially pathological instances for validating Alloy models. In: ICFEM, LNCS, vol. 10009, pp. 41–56 (2016)
47.
Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: CADE, LNCS, vol. 9195, pp. 434–449. Springer (2015)
48.
Serna, J., Day, N.A., Farheen, S.: DASH: a new language for declarative behavioural requirements with control state hierarchy. In: RE Workshops, pp. 64–68. IEEE Computer Society (2017)
49.
Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. Electron. Notes Discrete Math. 9, 19–35 (2001) CrossRefMATH
50.
Siegel, A., Santomauro, M., Dyer, T., Nelson, T., Krishnamurthi, S.: Prototyping formal methods tools: a protocol analysis case study. In: Protocols, Logic, and Strands: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday, LNCS. Springer (2021).
51.
Sullivan, A., Marinov, D., Khurshid, S.: Solution enumeration abstraction: a modeling idiom to enhance a lightweight formal method. In: ICFEM, LNCS, vol. 11852, pp. 336–352. Springer (2019)
52.
Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: ICST, pp. 264–275. IEEE (2017)
53.
Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: TACAS, LNCS, vol. 4424, pp. 632–647. Springer (2007)
54.
Uzuncaova, E., Khurshid, S.: Constraint prioritization for efficient analysis of declarative models. In: FM, LNCS, vol. 5014, pp. 310–325. Springer (2008)
55.
Vakili, A., Day, N.A.: Temporal logic model checking in Alloy. In: ABZ, LNCS, vol. 7316, pp. 150–163. Springer (2012)
56.
Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: IJCAI, pp. 298–303. Morgan Kaufmann (1995)
57.
Zheng, G., Bagheri, H., Rothermel, G., Wang, J.: Platinum: reusing constraint solutions in bounded analysis of relational logic. In: FASE, LNCS, vol. 12076, pp. 29–52. Springer (2020)
Metadaten
Titel
Pardinus: A Temporal Relational Model Finder
verfasst von
Nuno Macedo
Julien Brunel
David Chemouil
Alcino Cunha
Publikationsdatum
12.09.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09642-2

Weitere Artikel der Ausgabe 4/2022

Journal of Automated Reasoning 4/2022 Zur Ausgabe

OriginalPaper

A Wos Challenge Met

OriginalPaper

Larry Wos: Visions of Automated Reasoning

OriginalPaper

A Formalization of Dedekind Domains and Class Groups of Global Fields

OriginalPaper

Set of Support, Demodulation, Paramodulation: A Historical Perspective

OriginalPaper

Fast Left Kan Extensions Using the Chase

Correction

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic

Premium Partner