Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A formal approach to AADL model-based software engineering

  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large systems. In this paper, we report our experience in the formal verification of safety-critical real-time systems. We propose a formal mapping for a real-time task model using the LNT language, and we describe how it is used for the integration of a formal verification phase in an AADL model-based development process. We focus on real-time systems with event-driven tasks, asynchronous communication and preemptive fixed-priority scheduling. We provide a complete tool-chain for the automatic model transformation and formal verification of AADL models. Experimentation illustrates our results with the Flight control system and Line follower robot case studies.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15

Similar content being viewed by others

Notes

  1. Society of Automotive Engineers.

  2. LNT is developed by the VASY and CONVECS teams from Inria for safety-critical systems.

  3. More details about our AADL subset are provided in the AADL2LNT transformation definition (Sect. 4).

  4. A protected object is a construction based on the well-known concept of monitors for synchronizations.

  5. https://github.com/OpenAADL/ocarina.

  6. http://cadp.inria.fr/.

  7. The AADL2LNT transformation is integrated in the official Ocarina GitHub repository.

  8. The FCS and the LFR AADL models are available on-line in the AADLib GitHub repository, which is a library of reusable AADLv2 models under the OpenAADL project (https://github.com/OpenAADL/AADLib).

  9. https://github.com/OpenAADL/AADLib/tree/master/examples.

  10. Processor Intel Xeon(R), 2.20 GHz x32, 63GB RAM, running Linux MATE 1.12.

References

  1. AS5506A: SAE Architecture Analysis and Design Language (AADL) Version 2.0 (2009)

  2. AS5506/2: SAE Architecture Analysis and Design Language (AADL) Annex Volume 2 (2011)

  3. Abdoul, T., Champeau, J., Dhaussy, P., Pillain, P.Y., Roger, J.: AADL execution semantics transformation for formal verification. In: 13th IEEE International Conference on Engineering of Complex Computer Systems, pp. 263–268. IEEE (2008)

  4. Bae, K., Ölveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering, pp. 651–667. Springer, Berlin (2011)

    Chapter  Google Scholar 

  5. Bae, K., Ölveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods, pp. 94–109. Springer, Cham (2014)

    Chapter  Google Scholar 

  6. Bae, K., Ölveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering, pp. 59–62. Springer, Berlin (2012)

    Chapter  Google Scholar 

  7. Berthomieu, B., Bodeveix, J.P., Chaudet, C., Dal Zilio, S., Filali, M., Vernadat, F.: Formal verification of AADL specifications in the TOPCASED environment. In: Kordon, F., Kermarrec, Y. (eds.) Reliable Software Technologies—Ada-Europe 2009, pp. 207–221. Springer, Berlin (2009)

    Chapter  Google Scholar 

  8. Besnard, L., Bouakaz, A., Gautier, T., Le Guernic, P., Ma, Y., Talpin, J.P., Yu, H.: Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony. Sci. Comput. Program. 106, 54–77 (2015)

    Article  Google Scholar 

  9. Bodeveix, J.P., Filali, M., Garnacho, M., Spadotti, R., Yang, Z.: Towards a verified transformation from AADL to the formal component-based language FIACRE. Sci. Comput. Program. 106, 30–53 (2015). (Special Issue: Architecture-Driven Semantic Analysis of Embedded Systems)

    Article  Google Scholar 

  10. Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) Computer Safety, Reliability, and Security, pp. 173–186. Springer, Berlin (2009)

    Chapter  Google Scholar 

  11. Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54(5), 754–775 (2010)

    Article  Google Scholar 

  12. Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M., Wimmer, R.: A model checker for AADL. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, pp. 562–565. Springer, Berlin (2010)

    Chapter  Google Scholar 

  13. Burns, A.: The Ravenscar profile. ACM SIGAda Ada Lett. 19(4), 49–52 (1999)

    Article  Google Scholar 

  14. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Lang, F., McKinty, C., Powazny, V., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator. Technical report (2018)

  15. Chkouri, M.Y., Robert, A., Bozga, M., Sifakis, J.: Translating AADL into BIP-application to the verification of real-time systems. In: Chaudron, M.R.V. (ed.) Models in Software Engineering, pp. 5–19. Springer, Berlin (2009)

    Chapter  Google Scholar 

  16. Courtiat, J.P., Santos, C.A., Lohr, C., Outtaj, B.: Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Comput. Commun. 23(12), 1104–1123 (2000)

    Article  Google Scholar 

  17. Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) Fundamental Approaches to Software Engineering, pp. 111–126. Springer, Berlin (2011)

    Chapter  Google Scholar 

  18. Feiler, P., Gluch, D.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. SEI Series in Software Engineering. Pearson Education, London (2012)

    Google Scholar 

  19. Garavel, H., Hautbois, R.P.: An experiment with the LOTOS formal description technique on the flight warning computer of airbus 330/340 aircrafts. In: Proceedings of the first AMAST International Workshop on Real-Time Systems. Citeseer (1993)

  20. Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Formal Techniques for Networked and Distributed Systems, pp. 377–392. Springer, Boston (2001)

    Google Scholar 

  21. Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Inform. 52(4), 337–392 (2015)

    Article  MathSciNet  Google Scholar 

  22. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013)

    Article  Google Scholar 

  23. Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd: Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, pp. 3–26. Springer, Cham (2017)

    Chapter  Google Scholar 

  24. Garavel, H., Serwe, W.: State space reduction for process algebra specifications. Theor. Comput. Sci. 351, 131–145 (2006)

    Article  MathSciNet  Google Scholar 

  25. Geniet, D., Dubernard, J.P.: Scheduling hard sporadic tasks with regular languages and generating functions. Theor. Comput. Sci. 313(1), 119–132 (2004)

    Article  MathSciNet  Google Scholar 

  26. Gui, S., Luo, L., Li, Y., Wang, L.: Formal schedulability analysis and simulation for AADL. In: 2008 International Conference on Embedded Software and Systems, pp. 429–435. IEEE (2008)

  27. Hamdane, M.E., Chaoui, A., Strecker, M.: From AADL to timed automaton-a verification approach. Int. J. Softw. Eng. Appl. 7(4), 115–126 (2013)

    Google Scholar 

  28. Hamid, I., Najm, E.: Real-time connectors for deterministic data-flow. In: 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2007), pp. 173–182. IEEE (2007)

  29. Hamid, I., Najm, E.: Operational semantics of Ada Ravenscar. In: Kordon, F., Vardanega, T. (eds.) Reliable Software Technologies—Ada-Europe 2008, pp. 44–58. Springer, Berlin (2008)

    Chapter  Google Scholar 

  30. Hecht, M., Lam, A., Vogl, C.: A tool set for integrated software and hardware dependability analysis using the architecture analysis and design language (AADL) and error-model annex. In: 2011 16th IEEE International Conference on Engineering of Complex Computer Systems, pp. 361–366 (2011)

  31. Hu, K., Zhang, T., Yang, Z., Tsai, W.T.: Exploring AADL verification tool through model transformation. J. Syst. Archit. 61(3), 141–156 (2015)

    Article  Google Scholar 

  32. Jahier, E., Halbwachs, N., Raymond, P., Nicollin, X., Lesens, D.: Virtual execution of AADL models via a translation into synchronous programs. In: Proceedings of the 7th ACM and IEEE International Conference on Embedded Software, pp. 134–143. ACM, New York, NY, USA (2007)

  33. Johnsen, A., Lundqvist, K., Hanninen, K., Pettersson, P., Torelm, M.: AQAF: an architecture quality assurance framework for systems modeled in AADL. In: 2016 12th International ACM SIGSOFT Conference on Quality of Software Architectures (QoSA), pp. 31–40. IEEE (2016)

  34. Johnsen, A., Lundqvist, K., Pettersson, P., Jaradat, O.: Automated verification of AADL-specifications using UPPAAL. In: 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering, pp. 130–138. IEEE (2012)

  35. Lasnier, G., Zalila, B., Pautet, L., Hugues, J.: Ocarina: an environment for AADL models analysis and automatic code generation for high integrity applications. In: Kordon, F., Kermarrec, Y. (eds.) Reliable Software Technologies—Ada-Europe 2009, pp. 237–250. Springer, Berlin (2009)

    Chapter  Google Scholar 

  36. Léonard, L., Leduc, G.: A formal definition of time in LOTOS. Form. Asp. Comput. 10(3), 248–266 (1998)

    Article  Google Scholar 

  37. Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM 20(1), 46–61 (1973)

    Article  MathSciNet  Google Scholar 

  38. Lundqvist, K., Asplund, L.: A Ravenscar-compliant run-time kernel for safety-critical systems. Real Time Syst. 24(1), 29–54 (2003)

    Article  Google Scholar 

  39. Malavolta, I., Lago, P., Muccini, H., Pelliccione, P., Tang, A.: What industry needs from architectural languages: a survey. IEEE Trans. Softw. Eng. 39(6), 869–891 (2013)

    Article  Google Scholar 

  40. Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255–281 (2003). (Special issue on Formal Methods for Industrial Critical Systems)

    Article  MathSciNet  Google Scholar 

  41. Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008: Formal Methods, pp. 148–164. Springer, Berlin (2008)

    Chapter  Google Scholar 

  42. Mkaouar, H.: A formal approach for real-time systems engineering. Ph.D. thesis, University of Sfax, Tunisia (2019)

  43. Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: From AADL model to LNT specification. In: de la Puente, J.A., Vardanega, T. (eds.) Reliable Software Technologies—Ada-Europe 2015, pp. 146–161. Springer, Cham (2015)

    Chapter  Google Scholar 

  44. Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: An Ocarina extension for AADL formal semantics generation. In: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pp. 1402–1409. ACM, New York, NY, USA (2018)

  45. Ober, I., Halbwachs, N.: On the timed automata-based verification of Ravenscar systems. In: Kordon, F., Vardanega, T. (eds.) Reliable Software Technologies—Ada-Europe 2008, pp. 30–43. Springer, Berlin (2008)

    Chapter  Google Scholar 

  46. Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) Formal Techniques for Distributed Systems, pp. 47–62. Springer, Berlin (2010)

    Chapter  Google Scholar 

  47. Renault, X.: Mise en œuvre de notations standardisées, formelles et semi-formelles dans un processus de développement de systemes embarqués temps-réel répartis. Ph.D. thesis, Université Pierre et Marie Curie-Paris VI (2009)

  48. Renault, X., Kordon, F., Hugues, J.: Adapting models to model checkers, a case study: analysing AADL using Time or Colored Petri Nets. In: 2009 IEEE/IFIP International Symposium on Rapid System Prototyping, pp. 26–33. IEEE (2009)

  49. Renault, X., Kordon, F., Hugues, J.: From AADL architectural models to Petri Nets: Checking model viability. In: 2009 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC), pp. 313–320. IEEE (2009)

  50. Rolland, J.F., Bodeveix, J.P., Filali, M., Chemouil, D., Thomas, D.: Modes in asynchronous systems. In: 13th IEEE International Conference on Engineering of Complex Computer Systems (iceccs 2008), pp. 282–287. IEEE (2008)

  51. RTCA/DO-333: Formal Methods Supplement to DO-178C and DO-278A (2011)

  52. Rugina, A., Kanoun, K., KaÃćniche, M.: The ADAPT tool: From AADL architectural models to stochastic Petri nets through model transformation, pp. 85–90 (2008)

  53. Singhoff, F., Legrand, J., Nana, L., Marcé, L.: Cheddar: a flexible real time scheduling framework. In: ACM SIGAda Ada Letters, vol. 24, pp. 1–8. ACM (2004)

  54. Sokolsky, O., Lee, I., Clarke, D.: Schedulability analysis of AADL models. In: Proceedings of the 20th International Conference on Parallel and Distributed Processing, pp. 179–179. IEEE Computer Society, Washington, DC, USA (2006)

  55. Sokolsky, O., Lee, I., Clarke, D.: Process-algebraic interpretation of AADL models. In: Kordon, F., Kermarrec, Y. (eds.) Reliable Software Technologies—Ada-Europe 2009, pp. 222–236. Springer, Berlin (2009)

    Chapter  Google Scholar 

  56. Vyatkin, V.: Software engineering in industrial automation: state-of-the-art review. IEEE Trans. Ind. Inform. 9(3), 1234–1249 (2013)

    Article  Google Scholar 

  57. Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From AADL to Timed Abstract State Machines: A Verified Model Transformation, pp. 42–68. Elsevier, Amsterdam (2014)

    Google Scholar 

  58. Yu, H., Ma, Y., Gautier, T., Besnard, L., Le Guernic, P., Talpin, J.P.: Polychronous modeling, analysis, verification and simulation for timed software architectures. J. Syst. Archit. 59(10), 1157–1170 (2013)

    Article  Google Scholar 

  59. Yu, H., Ma, Y., Gautier, T., Besnard, L., Talpin, J.P., Le Guernic, P., Sorel, Y.: Exploring system architectures in AADL via Polychrony and SynDEx. Front. Comput. Sci. 7(5), 627–649 (2013)

    Article  MathSciNet  Google Scholar 

  60. Zhang, F., Zhao, Y., Ma, D., Niu, W.: Formal verification of behavioral AADL models by stateful timed CSP. IEEE Access 5, 27421–27438 (2017)

    Article  Google Scholar 

  61. Zhang, Y., Dong, Y., Zhang, Y., Zhou, W.: A study of the AADL mode based on timed automata. In: 2011 IEEE 2nd International Conference on Software Engineering and Service Science, pp. 224–227. IEEE (2011)

Download references

Acknowledgements

We would like to thank the CADP team (Hubert Garavel, Frédéric Lang and Wendelin Serwe) for their help in using the LNT language and CADP toolbox.

Author information

Authors and Affiliations

  1. ReDCAD Laboratory, University of Sfax, National School of Engineers of Sfax, BP 1173, 3038, Sfax, Tunisia

    Hana Mkaouar, Bechir Zalila & Mohamed Jmaiel

  2. Institut Supérieur de l’Aéronautique et de l’Espace (ISAE-SUPAERO), Université de Toulouse, 31055, Toulouse Cedex 4, France

    Jérôme Hugues

  3. Digital Research Center of Sfax, B.P. 275, 3021, Sakiet Ezzit, Sfax, Tunisia

    Mohamed Jmaiel

Authors
  1. Hana Mkaouar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bechir Zalila
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jérôme Hugues
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mohamed Jmaiel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hana Mkaouar.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Mkaouar, H., Zalila, B., Hugues, J. et al. A formal approach to AADL model-based software engineering. Int J Softw Tools Technol Transfer 22, 219–247 (2020). https://doi.org/10.1007/s10009-019-00513-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-019-00513-7

Keywords

Search

Navigation