Abstract
We present an automatable approach to verify that a system satisfies its requirements by verification of the program that controls the system. The approach can be applied if the interaction of the program with the system hardware can be faithfully described by a table relating domain phenomena and program variables. We show the applicability of the approach with a case study based on a real-world system.
Partly funded by the Ministry of Science and Culture (MWK) Baden-Württemberg in project “Verbundprojekt Salomo” ( www.salomo-projekt.de ).
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.
References
Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Bjørner, D.: Domains as a prerequisite for requirements and software domain perspectives and facets, requirements aspects and software views. In: Broy, M., Rumpe, B. (eds.) RTSE 1997. LNCS, vol. 1526, pp. 1–41. Springer, Heidelberg (1998)
Bjørner, D.: Domain engineering: A software engineering discipline in need of research. In: Hlavác, V., Jeffery, K.G., Wiedermann, J. (eds.) SOFSEM 2000. LNCS, vol. 1963, pp. 1–17. Springer, Heidelberg (2000)
Bjørner, D.: Domain engineering: a “Radical innovation” for software and systems engineering? A biased account. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 100–144. Springer, Heidelberg (2004)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: A declarative language for programming synchronous systems. In: POPL, pp. 178–188 (1987)
Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Halbwachs, N., Raymond, P., Ratel, C.: Generating Efficient Code From Data-Flow Programs. In: PLILP, vol. 22, pp. 207–218 (1991); special Issue on WOFACS 1998
Hall, A.: Realising the benefits of formal methods. J. UCS 13(5), 669–678 (2007)
IEC 61131 Programmable controllers, www.iec.ch
Jackson, D.: A Direct Path to Dependable Software. Commun. ACM 52(4), 78–88 (2009)
Jackson, M.: Software Requirements & Specifications: A Lexicon of Practice, Principles and Prejudices. ACM Press/Addison-Wesley Publishing Co., New York, NY, USA (1995)
Jackson, M., Zave, P.: Deriving specifications from requirements: An example. In: ICSE, pp. 15–24 (1995)
Jones, C.B.: Systematic software development using VDM. Prentice Hall International (UK) Ltd., Hertfordshire (1986)
Kant, E., Barstow, D.R.: The refinement paradigm: The interaction of coding and efficiency knowledge in program synthesis. IEEE Trans. Software Eng. 7(5), 458–471 (1981)
Lano, K.: The B Language and Method: A Guide to Practical Formal Development. Springer, New York (1996)
Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D. (eds.) FM 2009. LNCS, vol. 5850, pp. 806–809. Springer, Heidelberg (2009)
Nami, M.R., Tehrani, M.S., Sharifi, M.: Applying domain engineering using raise into a particular banking domain. SIGSOFT Softw. Eng. Notes 32(2), 1–6 (2007)
Seater, R., Jackson, D., Gheyi, R.: Requirement Progression in Problem Frames: Deriving Specifications from Requirements. Requir. Eng. 12(2), 77–102 (2007)
Snook, C.F., Harrison, R.: Practitioners’ views on the use of formal methods: an industrial survey by structured interview. Information & Software Technology 43(4), 275–283 (2001)
The RAISE Method Group: The RAISE Development Method. The BCS Practitioners Series, Prentice-Hall International, Englewood Cliffs (1995)
The Verifying C Compiler at Codeplex, http://vcc.codeplex.com/
Microsoft Visual Studio at MSDN, http://msdn.microsoft.com/en-us/vstudio/default.aspx
Westphal, B., Dietsch, D., Podelski, A., Pahlow, L.: Successful software subcontracting by system verification (submitted)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. 41(4), 1–36 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dietsch, D., Westphal, B., Podelski, A. (2011). System Verification through Program Verification. In: Butler, M., Schulte, W. (eds) FM 2011: Formal Methods. FM 2011. Lecture Notes in Computer Science, vol 6664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21437-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-21437-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21436-3
Online ISBN: 978-3-642-21437-0
eBook Packages: Computer ScienceComputer Science (R0)