Top

Empirical Software Engineering

Published in:

01-08-2014 | Experience Report

Experiences with incorporating formal techniques into industrial practice

Authors: Ammar Osaiweran, Mathijs Schuts, Jozef Hooman

Published in: Empirical Software Engineering | Issue 4/2014

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We report about experiences at Philips Healthcare with component-based development supported by formal techniques. The formal Analytical Software Design (ASD) approach of the company Verum has been incorporated into the industrial workflow. The commercial tool ASD:Suite supports both compositional verification and code generation for control components. For other components test-driven development has been used. We discuss the results of these combined techniques in a project which developed the power control service of an interventional X-ray system.

previous article Challenges and industry practices for managing software variability in small and medium sized enterprises

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York, NY, USACrossRefMATH

Beck K (2002) Test driven development: by example. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA

Bicarregui J, Fitzgerald J, Larsen PG, Woodcock J (2009) Industrial practice in formal methods: a review. In: Cavalcanti A, Dams D (eds) FM 2009: formal methods. Second World Congress, Lecture Notes in Computer Science, vol 5850. Springer-Verlag, pp 810–813

Broadfoot G (2005) Introducing formal methods into industry using cleanroom and CSP. Dedic Syst Mag, Tools Q1:1–13

Broadfoot GH, Broadfoot PJ (2003) Academia and industry meet: some experiences of formal methods in practice. In: 10th Asia-Pacific software engineering conference (APSEC 2003), pp 49–58

ClearSy, Atelier B (2011) Industrial tool supporting the B method. http://www.atelierb.eu/en/. Accessed Oct 2012

CSK Systems Corporation (2011) VDMTools. Industrial tool supporting VDM+ +. http://www.vdmtools.jp/en/. Accessed Oct 2012

Esterel Technologies (2011) SCADE Suite. Model based development environment dedicated to critical embedded software. http://www.esterel-technologies.com/products/scade-suite/. Accessed Oct 2012

Fitzgerald J, Larsen PG, Mukherjee P, Plat N, Verhoef M (2005) Validated designs for object-oriented systems. Springer, New York. Examples are available at http://www.vdmbook.com MATH

Formal Systems (2010) (Europe) Ltd and Oxford University computing laboratory: failures-divergence refinement – FDR2 user manual, 9th edn

Formal Systems (2011) (Europe) Ltd. FDR2 model checker. http://www.fsel.com. Accessed Oct 2012

Groote JF, Osaiweran A, Wesselius JH (2011) Analyzing the effects of formal methods on the development of industrial control software. In: Proceedings of the 27th IEEE ICSM 2011. Williamsburg, VA, USA, pp 467–472

Groote JF, Osaiweran A, Wesselius JH (2012) Experience report on developing the front-end client unit under the control of formal methods. In: Proceedings of the 27th ACM symposium on applied computing (SAC’12), ACM, pp 1183–1190

Hoare CAR (1985) Communicating sequential processes. Prentice-Hall

Hooman J, Huis in ’t Veld R, Schuts M (2011) Experiences with a compositional model checker in the healthcare domain. In: FHIES 2011, LNCS 7151, Springer-Verlag, pp 93–110, 2012 In: Pre-symposium Proceedings foundations of health information engineering and systems (FHIES 2011), pp 92–109. UNU-IIST Report 454, McSCert Report 5. http://www.iist.unu.edu/ICTAC/FHIES2011/Files/fhies2011_8_17.pdf

Hooman J (1991) Specification and compositional verification of real-time systems. Lecture notes in computer science, vol 558. Springer

Hopcroft PJ, Broadfoot GH (2005) Combining the box structure development method and CSP for software development. Electron Notes Theor Comp Sci 128(6):127–144CrossRef

IBM ClearCase (2011) http://www-01.ibm.com/software/awdtools/clearcase/. Accessed Oct 2012

Linger RC (1994) Cleanroom process model. IEEE Softw 11(2):50–58CrossRef

McConnell S (2004) Code complete, 2nd edn. Microsoft Press, Redmond, WA, USA

Mills HD (1988) Stepwise refinement and verification in box-structured systems. Comput 21:23–36CrossRef

Osaiweran A, Schuts M, Hooman J, Wesselius JH (2012) Incorporating formal techniques into industrial practice: an experience report. In: Proceedings of the 9th International workshop on formal engineering approaches to software components and architectures (FESCA’12) ENTCS (pages in press)

Osaiweran A, Groote JF, Schuts M, Hooman J, van Rijnsoever BJ (2012) Evaluating the effect of formal techniques in industry. Computer Science Report No. 12–13. Eindhoven: Technische Universiteit Eindhoven, pp 21

Prowell S, Trammell C, Linger R, Poore J (1999) Cleanroom software engineering: technology and process. Addison-Wesley

Prowell SJ, Poore JH (2003) Foundations of sequence-based software specification. IEEE Trans Softw Eng 29:417–429CrossRef

Schuts M (2010) Improving software development. Masters thesis, Radboud University Nijmegen, The Netherlands

Stellman A, Greene J (2005) Applied software project management. O’Reilly Media

TIOBE homepage (2011) http://www.tiobe.com. Accessed Oct 2012

Verum homepage (2011) http://www.verum.com. Accessed Oct 2012

Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J (2009) Formal methods: practice and experience. ACM Comput Surv 41(4):1–36CrossRef

Title: Experiences with incorporating formal techniques into industrial practice
Authors: Ammar Osaiweran
Mathijs Schuts
Jozef Hooman
Publication date: 01-08-2014
Publisher: Springer US
Published in: Empirical Software Engineering / Issue 4/2014
Print ISSN: 1382-3256
Electronic ISSN: 1573-7616
DOI: https://doi.org/10.1007/s10664-013-9251-2

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Other articles of this Issue 4/2014

Conducting quantitative software engineering studies with Alitheia Core

Correlations between bugginess and time-based commit characteristics

The impact of UML modeling on defect density and defect resolution time in a proprietary system

Data collection in global software engineering research: learning from past experience

Challenges and industry practices for managing software variability in small and medium sized enterprises

A family of experiments to assess the effectiveness and efficiency of source code obfuscation techniques

Premium Partner