Abstract
This paper presents the context-updates synthesis component of Chisel, a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. By context-updates we understand programming language constructs that induce unconditional control-flow non-sequentiality, i.e., gotos or subroutine calls. The context-updates synthesis follows two directions: an over-approximation phase that extracts a set of potential context-update constructs and an under-approximation phase that refines the results of the first step by testing the behavior of the context-updates constructs produced at the previous phase. We use two experimental semantics that cover two types of language paradigms: high-level imperative languages and low-level assembly languages and we conduct the tests on standard benchmarks used in avionics.
This research has been partially supported by the MINECO Spanish project TRACES (TIN2015-67522-C3-3-R) and by the Comunidad de Madrid project N-Greens Software-CM (S2013/ICE-2731).
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
Similar content being viewed by others
Notes
- 1.
- 2.
Please note that the underscore symbol _ represents a placeholder.
- 3.
The current implementation of Maude provides a terminating unification algorithm [6] for theories without axioms and for combinations of operators with the axioms A, C, AC, ACU, CU, U, Ul, and Ur (where A stands for associativity, C for commutativity, U for identity or unit, Ul for left identity or unit, and Ur for right identity or unit). If the theory does not fulfill the requirements it would be possible to implement a mechanism in Chisel to give a warning; however, for the time being we just focus on the syntheses mechanisms.
References
Abelson, H., Sussman, G.J.: Structure and Interpretation of Computer Programs. MIT Press, Cambridge (1985)
Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Combining runtime checking and slicing to improve Maude error diagnosis. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 72–96. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_3
Asăvoae, I.M., Asăvoae, M., Riesco, A.: Towards a formal semantics-based technique for interprocedural slicing. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 291–306. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_18
Asavoae, I.M., Asavoae, M., Riesco, A.: Context-updates analysis and refinement in Chisel. CoRR, abs/1709.06897 (2017)
Binkley, D., Gold, N., Harman, M., Islam, S., Krinke, J., Yoo, S.: ORBS: language-independent program slicing. In: FSE 2014, pp. 109–120 (2014)
Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude manual (Version 2.7.1), July 2016. http://maude.cs.uiuc.edu/maude2-manual
Clavel, M., Duran, F., Eker, S., Lincoln, P., Marti-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
Field, J., Ramalingam, G., Tip, F.: Parametric program slicing. In: POPL, pp. 379–392. ACM Press (1995)
Heintze, N., Riecke, J.G.: The sLam calculus: programming with secrecy and integrity. In: POPL, pp. 365–377 (1998)
Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, New York (1990)
Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. In: PLDI, pp. 35–46 (1988)
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015)
Kosmatov, N., Williams, N., Botella, B., Roger, M., Chebaro, O.: A lesson on structural testing with pathcrawler-online.com. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 169–175. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30473-6_15
Langdon, W.B., Yoo, S., Harman, M.: Inferring automatic test oracles. In: ICSE, pp. 5–6 (2017)
Meseguer, J., Rosu, G.: The rewriting logic semantics project. TCS 373(3), 213–237 (2007)
Nemer, F., Casse, H., Sainrat, P., Bahsoun, J.P., Michiel, M.D.: Papabench: a free real-time benchmark. In: WCET (2006)
Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: ICFP, pp. 123–135 (2014)
Riesco, A.: Using big-step and small-step semantics in Maude to perform declarative debugging. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 52–68. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07151-0_4
Riesco, A., Asăvoae, I.M., Asăvoae, M.: A generic program slicing technique based on language definitions. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 248–264. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37635-1_15
Riesco, A., Asavoae, I.M., Asavoae, M.: Memory policy analysis for semantics specifications in Maude. In: Falaschi, M. (ed.) LOPSTR 2015. LNCS, vol. 9527, pp. 293–310. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27436-2_18
Riesco, A., Asăvoae, I.M., Asăvoae, M.: Slicing from formal semantics: Chisel. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 374–378. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54494-5_21
Rosu, G.: K - a semantic framework for programming languages and formal analysis tools. In: Dependable Software Systems Engineering. IOS Press (2017)
Rosu, G.: Matching logic. Logical Methods in Computer Science (2017, to appear)
Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. New York University, Computer Science Department, New York, NY (1978)
Talpin, J., Jouvelot, P.: The type and effect discipline. In: LICS, pp. 162–173 (1992)
Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3(3), 121–189 (1995)
Weiser, M.: Program slicing. In: ICSE, pp. 439–449. IEEE Press (1981)
Acknowledgements
The authors would like to thank the anonymous reviewers for their valuable comments to improve the quality of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Asăvoae, I.M., Asăvoae, M., Riesco, A. (2018). Context-Updates Analysis and Refinement in Chisel. In: Gallardo, M., Merino, P. (eds) Model Checking Software. SPIN 2018. Lecture Notes in Computer Science(), vol 10869. Springer, Cham. https://doi.org/10.1007/978-3-319-94111-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-94111-0_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94110-3
Online ISBN: 978-3-319-94111-0
eBook Packages: Computer ScienceComputer Science (R0)