Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 8762))
Included in the following conference series:
522Accesses
Abstract
This paper presents a transformation-based compositional verification approach for verifying assumption-commitment properties. Our approach improves the verification process by pruning the state space of the model where the assumption is violated. This exclusion is performed by transformation functions which are defined based on a new notion of edges supporting a property. Our approach applies to all computational models where an automaton syntax with locations and edges induces a transition system semantics in a consistent way which is the case for hybrid, timed, Büchi, and finite automata. We have successfully applied our approach to Fischer’s protocol.
Partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center SFB/TR 14 AVACS (http://www.avacs.org).
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5491
- Price includes VAT (Japan)
- Softcover Book
- JPY 6864
- Price includes VAT (Japan)
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
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Andersen, H.R.: Partial model checking (extended abstract). In: LICS, pp. 398–407. IEEE Computer Society (1995)
Behrmann, G., David, A., Larsen, K.G.: A tutorial onuppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Benedetto, M.D.D., Gennaro, S.D., D’Innocenzo, A.: Verification of hybrid automata diagnosability by abstraction. IEEE TAC 56(9), 2050–2061 (2011)
Budkowski, S., Cavalli, A.R., Najm, E. (eds.): Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI / PSTV XVIII 1998, IFIP Conference Proceedings, vol, vol. 135. Kluwer (1998)
Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)
Damm, W.: Contract-based analysis of automotive and avionics applications: The SPEEDS approach. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 3–3. Springer, Heidelberg (2009)
Damm, W., et al.: Using contract-based component specifications for virtual integration testing and architecture design. In: DATE, pp. 1023–1028. IEEE (2011)
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE (1996)
Herbreteau, F., et al.: Lazy abstractions for timed automata. In: Sharygina et al. [20], pp. 990–1005
Janowska, A., Janowski, P.: Slicing timed systems. FI 60(1-4), 187–210 (2004)
Laarman, A., Olesen, M.C., et al.: Multi-core emptiness checking of timed büchi automata using inclusion abstraction. In: Sharygina et al. [20], pp. 968–983
Mahdi, A.: Compositional verification of computation path dependent real-time system properties. Master’s thesis, University of Freiburg (April 2012)
Muñiz, M., Westphal, B., Podelski, A.: Timed automata with disjoint activity. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 188–203. Springer, Heidelberg (2012)
Nielson, F., et al.: Principles of program analysis (2. corr. print). Springer (2005)
Olderog, E.R., Dierks, H.: Real-time systems. Cambridge University Press (2008)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)
SAE Int.: ARP-4761. Tech. rep., Aerospace Recommended Practice (1996)
Sangiovanni-Vincentelli, A.L., Damm, W., et al.: Taming Dr. Frankenstein: Contract-based design for cyber-physical systems. EJC 18(3), 217–238 (2012)
Sharygina, N., Veith, H. (eds.): CAV 2013. LNCS, vol. 8044. Springer, Heidelberg (2013)
Sher, F., Katoen, J.P.: Compositional abstraction techniques for probabilistic automata. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 325–341. Springer, Heidelberg (2012)
Xu, D.N., Jones, S.L.P., Claessen, K.: Static contract checking for Haskell. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 41–52. ACM (2009)
Author information
Authors and Affiliations
Carl von Ossietzky Universität, Ammerländer Heerstraße 114-118, 26111, Oldenburg, Germany
Ahmed Mahdi & Martin Fränzle
Albert-Ludwigs-Universität Freiburg, Georges-Köhler-Allee 52, 79110, Freiburg, Germany
Bernd Westphal
- Ahmed Mahdi
You can also search for this author inPubMed Google Scholar
- Bernd Westphal
You can also search for this author inPubMed Google Scholar
- Martin Fränzle
You can also search for this author inPubMed Google Scholar
Editor information
Editors and Affiliations
Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
Joël Ouaknine
Department of Computer Science, University of Liverpool, Liverpool, UK
Igor Potapov
Department of Computer Science, University of Oxford, UK
James Worrell
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Mahdi, A., Westphal, B., Fränzle, M. (2014). Transformations for Compositional Verification of Assumption-Commitment Properties. In: Ouaknine, J., Potapov, I., Worrell, J. (eds) Reachability Problems. RP 2014. Lecture Notes in Computer Science, vol 8762. Springer, Cham. https://doi.org/10.1007/978-3-319-11439-2_17
Download citation
Publisher Name:Springer, Cham
Print ISBN:978-3-319-11438-5
Online ISBN:978-3-319-11439-2
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative