Skip to main content
SpringerLink
Log in

Towards Formal Safety Analysis in Feature-Oriented Product Line Development

  • Conference paper
Foundations of Health Information Engineering and Systems (FHIES 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8315))

Abstract

Feature-orientation has proven beneficial in the development of software product lines. We investigate formal safety analysis and verification for product lines of software-intensive embedded systems. We show how to uniformly augment a feature-oriented, model-based design approach with the specification of safety requirements, failure models and fault injection. Therefore we analyze system hazards and identify the causes, i.e. failures and inadequate control systematically.

As features are the main concept of functional decomposition in the product line approach, features also direct the safety analysis and the specification of system level safety requirements: Safety (design) constraints are allocated to features. Subsequently, the behavior including possible faults is formally modeled. Then formal verification techniques are employed in order to prove that the safety constraints are satisfied and the system level hazards are prevented. We demonstrate our method using Scade Suite for the model-based product line design of cardiac pacemakers. VIATRA is employed for the model graph transformation generating the individual products. Formal safety analysis is performed by using Scade Design Verifier. The case study shows that our approach leads to a fine-grained safety analysis and is capable of uncovering unwanted feature interactions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Deneux, J., Stålmarck, G., Ågren, H., Åkerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115–129. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Apel, S., Kästner, C.: An overview of feature-oriented software development. Journal of Object Technology 8(5), 49–84 (2009)

    Article  Google Scholar 

  3. Azanza, M., Batory, D., Díaz, O., Trujillo, S.: Domain-specific composition of model deltas. In: Tratt, L., Gogolla, M. (eds.) ICMT 2010. LNCS, vol. 6142, pp. 16–30. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Bernstein, Daubert, Fletcher, Hayes, Lüderitz, Reynolds, Schoenfeld, Sutton: The revised NASPE/BPEG generic code for antibradycardia, adaptive-rate, and multisite pacing. Journal of Pacing and Clinical Electrophysiology 25, 260–264 (2002)

    Article  Google Scholar 

  5. Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic model checking of software product lines. In: Intern. Conf. on Software Engineering (ICSE), pp. 321–330 (2011)

    Google Scholar 

  6. Esterel Technologies: SCADE Suite KCG 6.1: Safety case report of KCG 6.1.2 (July 2009)

    Google Scholar 

  7. Feiler, P., Rugina, A.: Dependability modeling with the architecture analysis & design language (AADL). Tech. rep., Software Engineering Institute, CMU (July 2007)

    Google Scholar 

  8. Fischbein, D., Uchitel, S., Brabermann, V.: A foundation for behavioural conformance in software product line architectures. In: ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA), pp. 39–48. ACM (2006)

    Google Scholar 

  9. Ortmeier, F., Matthias Güdemann, W.R.: Formal failure models. In: 1st IFAC Workshop on Dependable Control of Discrete Systems, vol. 1, pp. 145–150 (2007)

    Google Scholar 

  10. Gray, J.G., Zhang, J., Lin, Y., Roychoudhury, S., Wu, H., Sudarsan, R., Gokhale, A.S., Neema, S., Shi, F., Bapty, T.: Model driven program transformation. In: Intern. Conf. on Generative Programming and Component Engineering (GPCE), pp. 361–378 (2004)

    Google Scholar 

  11. Haugen, Møller-Pedersen, Oldevik, Olsen, Svendsen: Adding standardized variability to domain specific languages. In: Intern. Software Product Line Conference, pp. 139–148. IEEE Computer Society (2008)

    Google Scholar 

  12. Huhn, M., Bessling, S.: Enhancing product line development by safety requirements and verification. In: Weber, J., Perseil, I. (eds.) FHIES 2012. LNCS, vol. 7789, pp. 37–54. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. IEC: 60812: Analysis techniques for system reliability

    Google Scholar 

  14. Jee, E., Lee, I., Sokolsky, O.: Assurance cases in model-driven development of the pacemaker software. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 343–356. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Jee, Wang, Kim, Lee, Sokolsky, Lee: A safety-assured development approach for real-time software. In: Proceedings of the 2010 IEEE 16th International Conference on Embedded and Real-Time Computing Systems and Applications, pp. 133–142. IEEE Computer Society, Washington, DC (2010), http://dx.doi.org/10.1109/RTCSA.2010.42

    Chapter  Google Scholar 

  16. Larson, B.R.: Integrated clinical environment patient-controlled analgesia infusion pump (January 2012)

    Google Scholar 

  17. Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety (Engineering Systems). The MIT Press (January 2012), http://www.worldcat.org/isbn/0262016621

  18. Liu, J., Basu, S., Lutz, R.R.: Compositional model checking of software product lines using variation point obligations. Autom. Softw. Eng. 18(1), 39–76 (2011)

    Article  Google Scholar 

  19. Liu, J., Dehlinger, J., Lutz, R.R.: Safety analysis of software product lines using state-based modeling. The Journal of Systems and Software 80, 1879–1892 (2007)

    Article  Google Scholar 

  20. OptXware Research and Development LLC: The Viatra-I model transformation framework pattern language specification

    Google Scholar 

  21. OptXware Research and Development LLC: The Viatra-I model transformation framework users’ guide

    Google Scholar 

  22. Pahl, G., Beitz, W., Feldhusen, J., Grote, K.H.: Pahl/Beitz Konstruktionslehre: Grundlagen erfolgreicher Produktentwicklung, 7. aufl. edn. Methoden und Anwendung. Springer, Berlin (2006), http://link.springer.com/book/10.1007/978-3-540-34061-4/page/1

  23. Schaefer, I., Gurov, D., Soleimanifard, S.: Compositional algorithmic verification of software product lines. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 184–203. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Schobbens, P.-Y., Heymans, P., Trigaux, J.-C.: Feature diagrams: A survey and a formal semantics. In: Intern. Conf. on Requirements Engineering (RE), pp. 136–145 (2006)

    Google Scholar 

  25. Scientific, B.: PACEMAKER System Specification (January 2007)

    Google Scholar 

  26. Thomas, J.: Extending and automating a systems-theoretic hazard analysis for requirements generation and analysis. Tech. rep., SANDIA National Laboratories (July 2012)

    Google Scholar 

  27. Tuan, Zheng, Tho: Modeling and verification of safety critical systems: A case study on pacemaker. In: 4th Conf. on Secure Software Integration and Reliability Improvement, pp. 23–32. IEEE (2010)

    Google Scholar 

  28. Varró, D., Varró, G., Pataricza, A.: Designing the automatic transformation of visual languages. Science of Computer Programming 44(2), 205–227 (2002)

    Article  MATH  Google Scholar 

  29. Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault Tree Handbook. U.S. Nuclear Regulatory Commission, Washington, DC (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, Clausthal University of Technology, Clausthal-Zellerfeld, Germany

    Sara Bessling & Michaela Huhn

Authors
  1. Sara Bessling
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michaela Huhn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Jeremy Gibbons

  2. Department of Mathematics, St. Francis Xavier University, P.O. Box 5000, B2G 2W5, Antigonish, NS, Canada

    Wendy MacCaull

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bessling, S., Huhn, M. (2014). Towards Formal Safety Analysis in Feature-Oriented Product Line Development. In: Gibbons, J., MacCaull, W. (eds) Foundations of Health Information Engineering and Systems. FHIES 2013. Lecture Notes in Computer Science, vol 8315. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-53956-5_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-53956-5_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-53955-8

  • Online ISBN: 978-3-642-53956-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation