Open Access Open Access  Restricted Access Subscription or Fee Access

Rapid Formal Verification as Requirements Stage Verification and Validation Technique


(*) Corresponding author


Authors' affiliations


DOI: https://doi.org/10.15866/irecos.v14i1.17684

Abstract


Early formal verification of a system during initial stages of development has the potential to improve the confidence in the system specifications, in addition to improving the formal verifiability throughout the software development cycle. A formal verification methodology is derived to achieve system modelling and verification during the requirements specification and system design phase. This is achieved by using Focus Stream theory for developing a formal system model derived from requirements analysis leading to a preliminary software design.  This results into component architecture and it incorporates the development of component behaviour using Finite Sate Machines. The models developed for real time system encompass modelling of infinite state domains. After model development, formal property enumeration under various categories is done. An enhanced safety property verification is proposed and implemented using Linear Temporal Logic propositions, pattern based properties and system safety based property patterns. Properties verification on the model is done in order to validate and refine the specifications. Derived properties are verified using NuXMV Satisfiability Modulo Theories based algorithms. Tool verification as mandated in RTCA DO-330 is incorporated in the proposed methodology. The proposed approach is practical, implementable by system designers and scalable to handle industrial systems.
Copyright © 2019 Praise Worthy Prize - All rights reserved.

Keywords


Formal Verification; Model Checking; Focus Stream Theory; Formal Modelling; Linear Temporal Logic; NuXMV; AutoFocus

Full Text:

PDF


References


RTCA Special Committee 167, Software Considerations in Airborne Systems and Equipment Certification, 1992.

RTCA Inc., DO-333 Formal Methods Supplement to DO-178C and DO-278A, 2011.

D. Cofer and S. P. Miller, Formal Methods Case Studies for DO-333, 2014.

X. Zheng and C. Julien, "Verification and Validation in Cyber Physical Systems: Research Challenges and a Way Forward," Proc. - Int. Work. Softw. Eng. Smart Cyber-Physical Syst. SEsCPS 2015, no. July 2015, pp. 15-18, 2015.
https://doi.org/10.1109/sescps.2015.11

E. M. Clarke, "The Birth of Model Checking," Link.Springer.Com, vol. 5000, no. Chapter 1, pp. 1-26, 2008.
https://doi.org/10.1007/978-3-540-69850-0_1

R. Alur, Model checking: From tools to theory, in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, vol. 5000 LNCS, pp. 89-106.
https://doi.org/10.1007/978-3-540-69850-0_6

F. Hölzl and M. Feilkas, AutoFocus 3 - A scientific tool prototype for model-based development of component-based, reactive, distributed systems, Lect. Notes Comput. Sci. (including Subser. Lect. Notes Artif. Intell. Lect. Notes Bioinformatics), vol. 6100 LNCS, pp. 317-322, 2010.
https://doi.org/10.1007/978-3-642-16277-0_13

R. Wang and S. Liu, TBFV-SE: Testing-Based Formal Verification with Symbolic Execution, 2018 IEEE Int. Conf. Softw. Qual. Reliab. Secur., pp. 59-66, 2018.
https://doi.org/10.1109/qrs.2018.00019

S. Haesaert, Progress Towards Flight Software Hybrid Controllers from Formal Specifications, 2018 IEEE Aerosp. Conf., pp. 1-17, 2018.
https://doi.org/10.1109/aero.2018.8396562

I. Filippidis, S. Dathathri, S. C. Livingston, N. Ozay, and R. M. Murray, Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox, 2016 IEEE Conf. Control Appl. CCA 2016, pp. 1030-1041, 2016.
https://doi.org/10.1109/cca.2016.7587949

V. Socci, Implementing a model-based design and test workflow, 1st IEEE Int. Symp. Syst. Eng. ISSE 2015 - Proc., pp. 130-134, 2015.
https://doi.org/10.1109/syseng.2015.7302745

S. Burmester, H. Giese, and W. Sch, Model Driven Architecture - Foundations and Applications, First European Conference, ECMDA-FA 2005, Nuremberg, Germany, November 7-10, 2005, Proceedings.

S. Tamblyn, J. Henry, and E. King, "A model-based design and testing approach for Orion GN&C flight software development," IEEE Aerosp. Conf. Proc., pp. 1-12, 2010.
https://doi.org/10.1109/aero.2010.5446802

C. Gamble, P. G. Larsen, and K. Pierce, Cyber-Physical Systems Design: Foundations, Methods, and Integrated Tool Chains John.Fitzgerald@ncl.ac.uk," 2015.
https://doi.org/10.1109/formalise.2015.14

Y. Yang, Y. Jiang, M. Gu, and J. Sun, Verifying Simulink Stateflow Model: timed automata approach, Proc. 31st IEEE/ACM Int. Conf. Autom. Softw. Eng. - ASE 2016, pp. 852-857, 2016.
https://doi.org/10.1145/2970276.2970293

J. F. Etienne, S. Fechter, and E. Juppeaux, Using simulink design verifier for proving behavioral properties on a complex safety critical system in the ground transportation domain, Proc. 1st Int. Conf. Complex Syst. Des. Manag. CSDM 2010, no. Dv, pp. 61-72, 2010.
https://doi.org/10.1007/978-3-642-15654-0_4

J. Yang, M. Ghazel, and E. M. El-Koursi, From formal specifications to efficient test scenarios generation, 2013 Int. Conf. Adv. Logist. Transp. ICALT 2013, pp. 35-40, 2013.
https://doi.org/10.1109/icadlt.2013.6568431

A. Dokhanchi, B. Hoxha, and G. Fainekos, Formal Requirement Elicitation and Debugging for Testing and Verification of Cyber-Physical Systems, Published in ArXiv 2016, vol. 17, no. 2, 2016.
https://doi.org/10.1145/3147451

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, Engineers use TLA+ to prevent serious but subtle bugs from reaching production. How Amazon Web Services Uses Formal Methods, Commun. Acm, vol. 58, no. 4, 2015.
https://doi.org/10.1145/2699417

J. Hugues, Open Archive Toulouse Archive Ouverte ( OATAO ) Tighter integration of drivers and protocols in a AADL-based code generation process, no. December, 2014.

J. O. Ringert, B. Rumpe, and A. Wortmann, From software architecture structure and behavior modeling to implementations of cyber-physical systems, Lect. Notes Informatics (LNI), Proc. - Ser. Gesellschaft fur Inform., vol. P-215, pp. 155-170, 2013.

H. Hildreth and J. D. Reese, Requirements Specification for Process-Control Systems, IEEE Trans. Softw. Eng., vol. 20, no. 9, pp. 684-707, 1994.
https://doi.org/10.1109/32.317428

C. Heitmeyer, a. Bull, C. Gasarch, and B. Labaw, SCR: a toolset for specifying and analyzing requirements, COMPASS '95 Proc. Tenth Annu. Conf. Comput. Assur. Syst. Integrity, Softw. Saf. Process Secur., pp. 109-122, 1995.
https://doi.org/10.1109/cmpass.1995.521891

S. Cranen et al., An overview of the mCRL2 toolset and its recent advances, Lect. Notes Comput. Sci. (including Subser. Lect. Notes Artif. Intell. Lect. Notes Bioinformatics), vol. 7795 LNCS, pp. 199-213, 2013.

F. Hö̈lzl, M. Spichkova, and D. Trachtenherz, AutoFocus Tool Chain, Focus (Madison)., p. 12, 2010.

M. Whalen, E. Anderson, M. Heimdahl, L. Wagner, and S. Miller, Formal Verification of Flight Critical Software, in AIAA Guidance, Navigation and Control Conference and Exhibit, 2005, no. August, pp. 1-16.
https://doi.org/10.2514/6.2005-6431

M. Bozga, L. Mounier, and D. Lesens, Model Checking Ariane-5 Flight Program Model Checking Ariane-5 Flight Program 1 Introduction, 2009.

S. P. Miller, A. C. Tribble, M. W. Whalen, and M. P. E. Heimdahl, Proving the shalls: Early validation of requirements through formal methods | Software Engineering Center, 2005.
https://doi.org/10.1007/s10009-004-0173-6

K. Pohl, H. Hönninger, R. Achatz, and M. Broy, Model-Based Engineering of Embedded Systems. 2012.
https://doi.org/10.1007/978-3-642-34614-9

M. Broy and K. Stolen, Specification and Development of Interactive Systems. 2001.
https://doi.org/10.1007/978-1-4613-0091-5

B. Kanso and O. Chebaro, Compositional Testing for Fsm-Based Models.2014. arXiv:1406.2808

N. Lynch, R. Segala, and F. Vaandrager, Hybrid I / O Automata Revisited, Esprit, pp. 403-417, 2001.
https://doi.org/10.1007/3-540-45351-2_33

O. Maler, Algorithmic Verification of Continuous and Hybrid Systems, Electron. Proc. Theor. Comput. Sci., vol. 140, pp. 48-69, 2014.
https://doi.org/10.4204/eptcs.140.4

S. Kanav and V. Aravantinos, Modular transformation from AF3 to nuXmv, CEUR Workshop Proc., vol. 2019, pp. 300-306, 2017.

F. F. Ü. R. Informatik and J. Thyssen, SPES 2020 Deliverable D1.3.A Einfuhrung in Analysetechniken Status, 2009.

S. Teufl, D. Mou, and D. Ratiu, MIRA: A tooling-framework to experiment with model-based requirements engineering, 2013 21st IEEE Int. Requir. Eng. Conf. RE 2013 - Proc., pp. 330-331, 2013.
https://doi.org/10.1109/re.2013.6636740


Refbacks

  • There are currently no refbacks.


Please send any question about this web site to info@praiseworthyprize.com
Copyright © 2005-2024 Praise Worthy Prize