Abstract
Most formal models that are used in the industry are close to the level of code, and often ready to be used for code generation. Formal models can also be analysed and verified in order to detect any faults. As the first formal models are often such code-level models, their analysis not only reveals a lot of detailed design faults, but also the more relevant conceptual faults in the design and the requirements. Our observations are based on our experiences in an industrial development project that uses a commercial tool for formal modelling, compositional verification, and code generation. In addition to the provided tool functionality, we have introduced formal techniques to detect conceptual faults during the earlier design and requirements phases. To this end we have made additional formal models, both for the requirements and for the early designs at various abstraction levels. We have analysed these models using simulation and interactive visualization, and we have compared them using refinement checking.
This publication was supported by the Allegio project, as part of the Dutch national program COMMIT, and the ITEA project Care4Me.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)
Blender, http://www.blender.org/
Boberg, J.: Early fault detection with model-based testing. In: Proceedings of Erlang Workshop 2008, pp. 9–20. ACM (2008)
von Bochmann, G.: Using First-Order Logic to Reason about Submodule Construction. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE 2009. LNCS, vol. 5522, pp. 213–218. Springer, Heidelberg (2009)
Broadfoot, G.H., Broadfoot, P.J.: Academia and industry meet: Some experiences of formal methods in practice. In: Proceedings of APSEC 2003, pp. 49–58 (2003)
ClearSy: Atelier B, http://www.atelierb.eu/en/
CSK Systems Corporation: VDMTools, http://www.vdmtools.jp/en/
Easterbrook, S.M., Lutz, R.R., Covington, R., Kelly, J., Ampo, Y., Hamilton, D.: Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering 24(1), 4–14 (1998)
Eindhoven University of Technology: Software/Hardware Engineering (SHE) - Parallel Object-Oriented Specification Language (POOSL), http://www.es.ele.tue.nl/poosl/
Esterel Technologies: SCADE Suite, http://www.esterel-technologies.com/products/scade-suite/
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-oriented Systems. Springer, New York (2005)
Fitzgerald, J.S., Larsen, P.G.: Balancing Insight and Effort: The Industrial Uptake of Formal Methods. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 237–254. Springer, Heidelberg (2007)
Formal Systems (Europe) Ltd: FDR2, http://www.fsel.com/
Formal Systems (Europe) Ltd and Oxford University Computing Laboratory: Failures-Divergence Refinement – FDR2 User Manual, 9th edn. (2010)
Goga, N., Romijn, J.: Guiding Spin Simulation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 176–193. Springer, Heidelberg (2004)
Groote, J.F., Osaiweran, A., Wesselius, J.H.: Analyzing the effects of formal methods on the development of industrial control software. In: Proceedings of ICSM 2011, pp. 467–472. IEEE (2011)
Haghverdi, E., Ural, H.: Submodule construction from concurrent system specifications. Information & Software Technology 41(8), 499–506 (1999)
Holzmann, G.J.: Early fault detection tools. Software - Concepts and Tools 17(2), 63–69 (1996)
Holzmann, G.J.: Formal Methods for Early Fault Detection. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 40–54. Springer, Heidelberg (1996)
Hooman, J., Huis in ’t Veld, R., Schuts, M.: Experiences with a Compositional Model Checker in the Healthcare Domain. In: George, C. (ed.) FHIES 2011. LNCS, vol. 7151, pp. 93–110. Springer, Heidelberg (2012)
Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP for software development. ENTCS 128(6), 127–144 (2005)
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Proceedings of LICS 1990, pp. 108–117. IEEE Computer Society (1990)
Li, L., Hooman, J., Voeten, J.: Connecting technical and non-technical views of system architectures. In: Proceedings of CPSCom 2010, pp. 592–599 (December 2010)
Roscoe, A.W., Armstrong, P.J., Pragyesh: Local Search in Model Checking. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 22–38. Springer, Heidelberg (2009)
Roscoe, B.: Understanding Concurrent Systems. Springer (2010)
Ryan, P.Y.A., Schneider, S.A., Goldsmith, M.H., Lowe, G., Roscoe, A.W.: The Modelling and Analysis of Security Protocols: the CSP Approach. Pearson Education (2000)
Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: Introducing a process analysis toolkit. In: Proceedings of ISoLA 2008. CCIS, vol. 17, pp. 307–322. Springer (2008)
Theelen, B.D., Florescu, O., Geilen, M., Huang, J., van der Putten, P.H.A., Voeten, J.: Software/hardware engineering with the parallel object-oriented specification language. In: Proceedings of MEMOCODE 2007, pp. 139–148. IEEE (2007)
Verum Software Technologies: ASD:Suite, http://www.verum.com/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hooman, J., Mooij, A.J., van Wezep, H. (2012). Early Fault Detection in Industry Using Models at Various Abstraction Levels. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)