nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)

verfasst von : Bernhard Steffen, Alnis Murtovi

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In this paper we position Linear Time Temporal Logic (LTL), structural operational semantics (SOS), and a graphical generalization of BNF as central DSLs for program analysis and verification tasks in order to illustrate the impact of language to the mindset: (1) Specifying program analyses in LTL changes the classical algorithmic ‘HOW’ thinking into a property-oriented ‘WHAT’ thinking that allows one to logically combine analysis goals and eases proofs. (2) Playing with the original store component in SOS configurations allows one to elegantly realize variants of abstract program interpretations, and to align different aspects, like e.g., the symbolic values of variables and path conditions. (3) Specializing languages by refining their BNF-like meta models has the power to lift certain verification tasks from the program to the programming language level. We will illustrate the advantages of the change of mindset imposed by these three DSLs, as well as the fact that these advantages come at low price due to available adequate generator technology.

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 Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)

Nächstes Kapitel Compositional Model Checking for Multi-properties

This work was based on bi-directional branching time temporal logics, which has later been replaced by bi-directional LTL.

\(\phi \, U \psi \), in contrast to \(\phi \, W \psi \), requires \(\psi \) to hold eventually.

Please note that the meaning of ‘state’ in this section only concerns \(\varSigma \), in contrast to the other sections, where ‘state’ denotes nodes of a transitions system.

For the sake of simplicity, we use an uniform assignment pattern \(x=a+b\) in the example. This allows us to eliminate complete statements without keeping track on temporaries. A detailed discourse on the issue of assignment vs. expression motion can be found in [22].

In a realistic setting minimization would take conditions of branching into account.

Alternatively, one can regard CFMTSs also as extensions of Context-Free Process Systems [5] to allow may transitions.

Modal refinement preserves properties specified in branching-time temporal logic [30].

The treatment of multiple procedures can be achieved either via a preprocess that constructs individual ‘A’-like properties for each procedure, or by enhancing the modeling language towards an adequate notion of Context-Free Modal Register Automata (cf. [16] for the definition of register automata). Whereas the former approach is rather straightforward the latter approach is part of our envisioned future work which, in particular, concerns the corresponding model checking problems.

Directed Acyclic Graph [56].

DTD stands for Document Type Descriptions.

This leads to very tolerant process specifications, similar to what is aimed at it with CMMN [38] in order to overcome the over specification easily imposed when using e.g. BPMN [37].

Xtext - Language Engineering Made Easy! http://www.eclipse.org/Xtext/. Accessed 16 Nov 2020

Bloom, B.: Structured operational semantics as a specification language. In: Cytron, R.K., Lee, P. (eds.) Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, 23–25 January 1995, pp. 107–117. ACM Press (1995)

Bradfield, J.C., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, pp. 721–756. North-Holland (2007)

Burkart, O., Caucal, D., Steffen, B.: Bisimulation collapse and the process taxonomy. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 247–262. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61604-7_59CrossRef

Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084787CrossRef

Chamberlin, D.D., Boyce, R.F.: SEQUEL: a structured English query language. In: Rustin, R. (ed.), Proceedings of 1974 ACM-SIGMOD Workshop on Data Description, Access and Control, Ann Arbor, Michigan, USA, 1–3 May 1974, vol. 2, pp. 249–264. ACM (1974)

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774CrossRef

Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8MATHCrossRef

Cleaveland, R., Madelaine, E., Sims, S.: A front-end generator for verification tools. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 153–173. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60630-0_8CrossRef

10.

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference on Record of the 4th, Los Angeles, CA, 1977, pp. 238–252 (1977)

11.

Dhamdhere, D.M.: A fast algorithm for code movement optimisation. ACM SIGPLAN Not. 23(10), 172–180 (1988)CrossRef

12.

Dhamdhere, D.M., Keith, J.S.: Characterization of program loops in code optimization. Comput. Lang. 8(2), 69–76 (1983)MATHCrossRef

13.

Emerson, E.A., Halpern, J.Y.: “sometimes” and “not never” revisited: on branching versus linear time. In: Wright, J.R., Landweber, L., Demers, A.J., Teitelbaum, T. (eds.) Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pp. 127–140. ACM Press (1983)

14.

Gossen, F., Jasper, M., Murtovi, A., Steffen, B.: Aggressive aggregation: a new paradigm for program optimization. CoRR, abs/1912.11281 (2019)

15.

Grundy, J., Hosking, J., Li, K.N., Ali, N.M., Huh, J., Li, R.L.: Generating domain-specific visual language tools from abstract visual specifications. IEEE Trans. Software Eng. 39(4), 487–515 (2013)CrossRef

16.

Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251–266. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_17CrossRef

17.

Jörges, S.: Construction and Evolution of Code Generators - A Model-Driven and Service-Oriented Approach. LNCS, vol. 7747. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36127-2CrossRef

18.

Jörges, S., Margaria, T., Steffen, B.: Genesys: service-oriented construction of property conform code generators. Innov. Syst. Softw. Eng. 4(4), 361–384 (2008)CrossRef

19.

Kats, L.C.L., Visser, E.: The spoofax language workbench: rules for declarative specification of languages and ides. In: Cook, W.R., Clarke, S., Rinard, M.C. (eds.) Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, Reno/Tahoe, Nevada, USA, 17–21 October 2010, pp. 444–463. ACM (2010)

20.

Kelly, S., Tolvanen, J.-P.: Domain-Specific Modeling: Enabling Full Code Generation. Wiley-IEEE Computer Society Press, Hoboken (2008)CrossRef

21.

Knoop, J., Rüthing, O., Steffen, B.: Partial dead code elimination. In: Proceedings of the 1994, Orlando, FL, June 1994, vol. 29, no. 6, pp. 147–158 (1994)

22.

Knoop, J., Rüthing, O., Steffen, B.: The power of assignment motion. In: Proceedings of the 1995, La Jolla, CA, June 1995, vol. 30, no. 6, pp. 233–245 (1995)

23.

Knoop, J., Rüthing, O., Steffen, B.: Expansion-based removal of semantic partial redundancies. In: Jähnichen, S. (ed.) CC 1999. LNCS, vol. 1575, pp. 91–106. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-540-49051-7_7CrossRef

24.

Knoop, J., Rüthing, O., Steffen, B.: Lazy code motion. In: Feldman, S.I., Wexelblat, R.L. (eds.) Proceedings of the ACM SIGPLAN 1992 Conference on Programming Language Design and Implementation (PLDI), San Francisco, California, USA, 17–19 June 1992, pp. 224–234. ACM (1992)

25.

Knoop, J., Rüthing, O., Steffen, B.: Lazy code motion (with retrospective). In: McKinley, K.S. (ed.) 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979–1999, A Selection, pp. 460–472. ACM (1992)

26.

Knuth, D.E.: Backus normal form vs. Backus Naur form. Commun. ACM 7(12), 735–736 (1964)CrossRef

27.

Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)MATHCrossRef

28.

Kripke, S.: Semantical considerations on modal logic. Acta Phil. Fennica 16, 83–94 (1963)MathSciNetMATH

29.

Larsen, K.G., Thomsen, B.: A modal process logic. In: [1988] Proceedings. Third Annual Symposium on Logic in Computer Science, pp. 203–210 (1988)

30.

Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_19CrossRef

31.

Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. Computer 43(6), 90–92 (2010)CrossRef

32.

Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle Rive (1989)

33.

Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Commun. ACM 22(2), 96–103 (1979)MathSciNetMATHCrossRef

34.

Müller-Olm, M., Schmidt, D., Steffen, B.: Model-Checking: a tutorial introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48294-6_22CrossRef

35.

Naujokat, S., Lybecait, M., Kopetzki, D., Steffen, B.: CINCO: a simplicity-driven approach to full generation of domain-specific graphical modeling tools. STTT 20(3), 327–354 (2018)CrossRef

36.

De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17CrossRef

37.

Object Management Group (OMG): Documents Associated with BPMN Version 2.0.1, September 2013. http://www.omg.org/spec/BPMN/2.0.1/. Accessed 16 Nov 2020

38.

Object Management Group (OMG): Documents Associated with Case Management Model and Notation (CMMN), Version 1.0, May 2014. http://www.omg.org/spec/CMMN/1.0/. Accessed 16 Nov 2020

39.

Plotkin, G.: A structural approach to operational semantics. Technical report, Aarhus Univ., Computer Science Dept., Denmark 1981. DAIMI FN-19

40.

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46–57. IEEE Computer Society (1977)

41.

Ray, E.T.: Learning XML - Creating Self-Describing Data: Cover Schemas, 2 edn. O’Reilly, Sebastopol (2003)

42.

Rüthing, O., Knoop, J., Steffen, B.: Detecting equalities of variables: combining efficiency with precision. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 232–247. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48294-6_15CrossRef

43.

Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: MacQueen, D.B., Cardelli, L. (eds.) Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1998, San Diego, CA, USA, 19–21 January 1998, pp. 38–48. ACM (1998)

44.

Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49727-7_22CrossRef

45.

Smyth, S.: Interactive model-based compilation. Ph.D. thesis, CAU Kiel, to appear

46.

Steffen, B., Knoop, J., Rüthing, O.: The value flow graph: a program representation for optimal program transformations. In: Jones, N. (ed.) ESOP 1990. LNCS, vol. 432, pp. 389–405. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52592-0_76CrossRef

47.

Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–364. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54415-1_54CrossRef

48.

Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115–139 (1993)MATHCrossRef

49.

Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 22–41. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61739-6_31CrossRef

50.

Steffen, B., Claßen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60218-6_6CrossRef

51.

Steffen, B., Gossen, F., Naujokat, S., Margaria, T.: Language-driven engineering: from general-purpose to purpose-specific languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 311–344. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9_17CrossRef

52.

Steffen, B., Murtovi, A.: M3C: modal meta model checking. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 223–241. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_15CrossRef

53.

Steffen, B., Naujokat, S.: Archimedean points: the essence for mastering change. Trans. Found. Mastering Chang. 1, 22–46 (2016)CrossRef

54.

Steffen, B., Rüthing, O.: Quality engineering: leveraging heterogeneous information. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 23–37. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_4CrossRef

55.

Tegeler, T., Murtovi, A., Frohme, M., Steffen, B.: Product line verification via modal meta model checking. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 313–337. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30985-5_19CrossRef

56.

Thulasiraman, K., Swamy, M.N.S.: Graphs - Theory and Algorithms. Wiley, New York (1992)MATHCrossRef

57.

Voelter, M., Pech, V.: Language modularity with the MPS language workbench. In: Glinz, M., Murphy, G.C., Pezzè, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, Zurich, Switzerland, 2–9 June 2012, pp. 1449–1450. IEEE Computer Society (2012)

58.

Völter, M., et al.: DSL Engineering - Designing, Implementing and Using Domain-Specific Languages (2013). dslbook.org

59.

Wirth, N.: Compilerbau - Eine Einführung. Teubner (1977)

Titel: Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)
verfasst von: Bernhard Steffen
Alnis Murtovi
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-67066-5

Electronic ISBN: 978-3-030-67067-2

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-67067-2_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"