Abstract
This paper presents a new technique for the generation of verification benchmarks that are automatically guaranteed to be hard, or as we say, to contain subtle bugs/property violations: (i) Identifying a bug requires to match many computation steps and (ii) corresponding counterexamples are sparse among all feasible executions. Key idea is to iteratively synthesize Büchi automata for variations of a set of LTL properties and to combine these automata in a fashion that each property can be individually controlled in the resulting model: Based on our notion of a counterexample handle, it is possible to switch the satisfaction of a given property on and off without affecting that of the other considered properties. This orthogonality of our treatment of counterexamples is vital for the subsequent parts of the benchmark generation process. Together with the mentioned hardness, it helps to overcome the undesired clustering of counterexamples observed during previous iterations of the RERS Challenge. Even more importantly, these handles and associated counterexamples are sufficient to automatically generate the modal contracts required for the parallel decomposition process that allows us to generate parallel verification benchmarks of arbitrary size, for example in form of a Petri net or in Promela.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
An execution is deep if it requires the observation of many computation steps.
- 2.
According to a news article (https://www.securityfocus.com/news/8016), a spokesman of an involved company said: “This fault was so deeply embedded, it took them weeks of poring through millions of lines of code and data to find it”.
- 3.
- 4.
Also called elementary circuit [16]: A simple cycle is a path \(s_1 {\mathop {\rightarrow }\limits ^{\sigma _1}} ... {\mathop {\rightarrow }\limits ^{\sigma _{n-1}}} s_n {\mathop {\rightarrow }\limits ^{\sigma _n}} s_1\) such that \(s_i \ne s_j\) for any \(i,j \in 1..n\) with \(i \ne j\).
- 5.
This refers to the matching of computation steps in our introduction. Here, we talk about transition symbols because the BA has not been transformed to a final code model yet.
- 6.
A simple path visits each state at most once.
- 7.
Let \(B'\) be a modified version of BA B where all transitions \(t \in \{ t \text { }|\text { }(\psi , t) \in H \}\) have been removed. Then state \(u_0\) is still reachable in \(B'\).
- 8.
Details can be found in [15].
- 9.
For example, semantic interference between properties in \(\varPhi \) can be the reason why no \(\phi \)-OCE-extension exists: If \(\phi \) is implied by the formula \(\bigwedge _{\psi \in \varPsi } \psi \) with \(\varPsi \subseteq \{ \psi \in \varPhi \text { }|\text { }B \models \psi \wedge \psi \ne \phi \}\), then the language \(\mathcal {L}_{\varPhi }^{\lnot \phi }\) has to be empty.
- 10.
Here, we say that a counterexample for \(\phi \) is detected once the corresponding path can no longer satisfy \(\phi \). Due to Definition 6, this implies an existing counterexample.
- 11.
The synthesized Büchi automata illustrated within this paper were generated using SPOT [6] and modified regarding their visualization.
- 12.
An input OCEBA has to adhere to an additional constraint, however it is guaranteed to do so if it was generated using Algorithm 1. See the next sub-section for details.
- 13.
Details can be found in [15].
- 14.
Refinement will be formally specified in Definition 24.
- 15.
Note that modal refinement which expands the MTS M can also be used if the CE-handle and witness information is updated accordingly.
- 16.
A property profile is a map from benchmark properties that need to be checked on a given program to their correct true/false valuation for that program.
- 17.
In contrast to the technique presented in this paper, the approach of [29] only preserves a subset of temporal properties. This subset is very expressive as it covers many common LTL patterns.
- 18.
References
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)
Bartocci, E., et al.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. STTT 1–40 (2017). https://doi.org/10.1007/s10009-017-0454-5
Büchi, J.R.: Symposium on decision problems: on a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science, Studies in Logic and the Foundations of Mathematics, vol. 44, pp. 1–11. Elsevier (1966)
Beyer, D.: Competition on software verification. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_38
Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_31
Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized Büchi automata. In: 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS 2004), pp. 76–83. IEEE (2004)
Erickson, K.T.: Programmable logic controllers. IEEE Potentials 15(1), 14–17 (1996). https://doi.org/10.1109/45.481370
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_6
Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 787–803. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_59
Gourcuff, V., Smet, O.D., Faure, J.M.: Efficient representation for formal verification of PLC programs. In: 2006 8th International Workshop on Discrete Event Systems, pp. 182–187, July 2006
Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Păsăreanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. STTT 16(5), 457–464 (2014)
Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012. STTT 17(6), 647–657 (2015)
Jasper, M., et al.: The RERS 2017 challenge and workshop (invited paper). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pp. 11–20. ACM (2017)
Jasper, M., Schordan, M.: Multi-core model checking of large-scale reactive systems using different state representations. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 212–226. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_15
Jasper, M., Steffen, B.: Synthesizing verification benchmarks with subtle bugs for given property profiles. (To appear)
Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM J. Comput. 4(1), 77–84 (1975)
Kordon, F.: Report on the model checking contest at petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169–196. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35179-2_8
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_19
Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045–1079 (1955)
Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)
Moon, I.: Modeling programmable logic controllers for logic verification. IEEE Control Syst. 14(2), 53–59 (1994)
Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River (1981)
Plotkin, G.D.: A structural approach to operational semantics. DAIMI FN-19, Computer Science Department, Aarhus University (1981)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989, pp. 179–190. ACM, New York (1989)
Rausch, M., Krogh, B.H.: Formal verification of PLC programs. In: Proceedings of the 1998 American Control Conference, ACC, vol. 1, pp. 234–238, June 1998
Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark petri nets. In: 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 1–8, June 2017
Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. STTT 16(5), 543–558 (2014)
Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. STTT 16(5), 465–479 (2014)
Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 125–145. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_7
Visser, W., Mehlitz, P.: Model checking programs with Java PathFinder. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, p. 27. Springer, Heidelberg (2005). https://doi.org/10.1007/11537328_5
Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1), 72–99 (1983)
Zhivich, M., Cunningham, R.K.: The real cost of software errors. IEEE Secur. Priv. 7(2), 87–90 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Jasper, M., Steffen, B. (2018). Synthesizing Subtle Bugs with Known Witnesses. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-03421-4_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03420-7
Online ISBN: 978-3-030-03421-4
eBook Packages: Computer ScienceComputer Science (R0)