Abstract
Developers who use C model checkers have to overcome three usability challenges: First, it is difficult to express application level properties as C-level verification conditions, due to the abstraction gap. Second, without advanced IDE support, it is difficult to interpret the counterexamples produced by the model checker and understand what went wrong in terms of application level properties. Third, most C model checkers support only a subset of C and it is easy for developers to inadvertently use C constructs outside this subset. In this paper we report on our preliminary experience with using the MPS language workbench to integrate the CBMC model checker with a set of domain-specific extensions of C for developing embedded software. Higher level language constructs such as components and decision tables makes it easier for end users to bridge the abstraction gap, to write verification conditions and to interpret the analysis results. Furthermore, the use of language workbenches allows the definition of analyzable language subsets, making the implementation of analyses simpler and their use more predictable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Loer, K., Harrison, M.: Towards Usable and Relevant Model Checking Techniques for the Analysis of Dependable Interactive Systems. In: ASE (2002)
Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Păsăreanu, C., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE 2000 (2000)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Voelter, M., Ratiu, D., Schätz, B., Kolb, B.: mbeddr: an extensible c-based programming language and ide for embedded systems. In: SPLASH 2012 (2012)
Voelter, M.: Language and IDE Modularization and Composition with MPS. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2011. LNCS, vol. 7680, pp. 383–430. Springer, Heidelberg (2013)
Ratiu, D., Voelter, M., Schaetz, B., Kolb, B.: Language Engineering as Enabler for Incrementally Defined Formal Analyses. In: FORMSERA 2012 (2012)
Ratiu, D., Markus Voelter, Z.M., Schaetz, B.: Implementing modular domain specific languages and analyses. In: MoDEVVa 2012 (2012)
Janicki, R., Parnas, D.L., Zucker, J.: Tabular representations in relational documents. In: Relational Methods in Computer Science (1997)
Beyer, D., Henzinger, T., Jhala, R., Majumdar, R.: An eclipse plug-in for model checking. In: IWPC 2004 (2004)
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)
Zalila, F., Crégut, X., Pantel, M.: Leveraging formal verification tools for DSML users: A process modeling case study. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 329–343. Springer, Heidelberg (2012)
Combemale, B., Gonnord, L., Rusu, V.: A Generic Tool for Tracing Executions Back to a DSML’s Operational Semantics. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 35–51. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ratiu, D., Voelter, M., Kolb, B., Schaetz, B. (2013). Using Language Engineering to Lift Languages and Analyses at the Domain Level. In: Brat, G., Rungta, N., Venet, A. (eds) NASA Formal Methods. NFM 2013. Lecture Notes in Computer Science, vol 7871. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38088-4_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-38088-4_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38087-7
Online ISBN: 978-3-642-38088-4
eBook Packages: Computer ScienceComputer Science (R0)