Formal Verification of Complex Systems based on SysML Functional Requirements
##plugins.themes.bootstrap3.article.main##
##plugins.themes.bootstrap3.article.sidebar##
Abstract
As modern systems continue to increase in size and complexity, they pose increasingly significant safety and risk management challenges. A model-based safety approach is an efficient way of coping with the increasing system complexity. It helps better manage the complexity by utilizing reasoning tools that require abstract models to detect failures as early as possible during the design process. This paper develops a methodology for the verification of safety requirements for design of complex engineered systems. The proposed approach combines a SysML modeling approach to document and structure safety requirements, and an assume-guarantee technique for the formal verification purpose. The assume- guarantee approach, which is based on a compositional and hierarchical reasoning combined with a learning algorithm, is able to simplify complex design verification problems. The objective of the proposed methodology is to integrate safety into early design stages and help the system designers to consider safety implications during conceptual design synthesis, reducing design iterations and cost. The proposed approach is validated on the quad-redundant Electro-Mechanical Actuator (EMA) of a Flight Control Surface (FCS) of an aircraft.
How to Cite
##plugins.themes.bootstrap3.article.details##
early system design, failure prognosis, Verification, safety analysis
ARP4761, S. (1996). Guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment. SAE International, December.
Balaban, E., Saxena, A., Goebel, K., Byington, C., Watson, M., Bharadwaj, S., Amin, S. (2009). Experimental Data Collection And Modeling For Nominal And Fault Conditions On Electromechanical Actuators. In Annual conference of the prognostics and health management society (pp. 1–15).
Baroth, E., Zakrajsek, J., Powers, W., Fox, J., Prosser, B., Pal.lix, J., & Schweikard, K. (2001). Ivhm (Integrated Vehicle Health Management) techniques for future space vehicles. In 37th joint propulsion conference.
Barragan, I. S., Roth, M., Faure, J.-M., et al. (2006). Obtain- ing temporal and timed properties of logic controllers from fault tree analysis. In Proceedings of the 12th ifac symposium on information control problems in manufacturing, incom 2006, saint-etienne, France.
Blaise, J.-C., Lhoste, P., & Ciccotelli, J. (2003). Formalization of normative knowledge for safe design. Safety Science, 41(2), 241–261.
Blanchard, B. S. (2012). System engineering management (Vol. 64). Wiley. com.
Buede, D. M. (2011). The engineering design of systems: Models and methods (Vol. 55). John Wiley & Sons.
Chaki, S., Clarke, E., Sinha, N., & Thati, P. (2005). Automated Assume-guarantee Reasoning for Simulation Conformance. In Computer aided verification (pp. 241–246).
Cobleigh, J. M., Giannakopoulou, D., & Pa ̆sa ̆reanu, C. S. (2003). Learning Assumptions For Compositional Verification. In Tools and algorithms for the construction and analysis of systems (pp. 331–346). Springer.
Evrot, D., Petin, J.-F., & Mery, D. (2006). Formal specification of safe manufacturing machines using the b method: Application to a mechanical. In Information control problems in manufacturing (Vol. 12, pp. 281– 286).
GeenSys. (2008). Reqtify. www.geensys.com. Giannakopoulou, D., Pa ̆sa ̆reanu, C. S., & Barringer, H. (2005). Component Verification With Automatically Generated Assumptions. Automated Software Engineering, 12(3), 297–320.
Giannakopoulou, D., Pasareanu, C. S., & Cobleigh, J. M.(2004). Assume-guarantee verification of source code with design-level assumptions. In Proceedings of the 26th international conference on software engineering (pp. 211–220).
Henzinger, T. A., Ho, P., & Wong-Toi, H. (1997). Hytech: A Model Checker for Hybrid Systems. Electronics Research Laboratory, College of Engineering, University of California..
Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic Model Checking for Real-time Systems. Information and Computation, 111(2), 193-244.
Henzinger, T. A., Qadeer, S., & Rajamani, S. K. (1998). You assume, we guarantee: Methodology and case studies. In Computer aided verification (pp. 440–451).
Hirtz, J., Stone, R. B., McAdams, D. A., Szykman, S., & Wood, K. L. (2002). A Functional Basis For Engineering Design: Reconciling And Evolving Previous Efforts. Research in engineering Design, 13(2), 65– 82.
Hollnagel, E., Woods, D. D., & Leveson, N. (2007). Resilience engineering: Concepts and precepts. Ashgate Publishing, Ltd.
IBM. (2010). Rational doors. Available from: http://www- 01.ibm.com/software/awdtools/doors.
IEC. (1998). 61508 functional safety of electrical/electronic/programmable electronic safety-related systems. International electrotechnical commission.
IEEE1220. (2005). IEEE standard for application and management of the systems engineering process. IEEE New
York, NY, USA.
ISO-IEC15288. (2002). Systems engineering system life cycle processes. International Standardization Organization.
Kurtoglu, T., & Campbell, M. I. (2009). Automated Synthesis Of Electromechanical Design Configurations From Empirical Analysis Of Function To Form Mapping. Journal of Engineering Design, 20(1), 83–104.
Kurtoglu, T., & Tumer, I. Y. (2008). A graph-based fault identification and propagation framework for functional design of complex systems. Journal of Mechanical Design, 130(5), 051401.
Leveson, N. (2011). Engineering a safer world: Systems thinking applied to safety. MIT Press.
Leveson, N. G. (2009). The need for new paradigms in safety engineering. In Safety-critical systems: Problems, process and practice (pp. 3–20). Springer.
Lundteigen, M. A., Rausand, M., & Utne, I. B. (2009). Integrating rams engineering and management with the safety life cycle of iec 61508. Reliability Engineering & System Safety, 94(12), 1894–1903.
Madni, A. (2007). Designing for resilience. ISTI Lecture Notes on Advanced Topics in Systems Engineering.
Nagel, R. L., Stone, R. B., Hutcheson, R. S., McAdams, D. A., & Donndelinger, J. A. (2008). Function Design Framework (FDF): Integrated Process And Function Modeling For Complex Systems. In Asme 2008 international design engineering technical conferences & computers and information in engineering conference (idetc/cie 2008) (pp. 273–286).
Nam, W., & Alur, R. (2006). Learning-based Symbolic Assume-guarantee Reasoning With Automatic decomposition. In Automated technology for verification and analysis (pp. 170–185). Springer.
OMG, O. (2007). Unified modeling language (omg uml). Superstructure.
Rodrigues, R. W. (2000). Formalising UML Activity Diagrams Using Finite State Processes. In Proc. of the 3rd intl. conf. on the unified modeling language, york, uk.
Stone, R. B., Tumer, I. Y., & Stock, M. E. (2005). Link- ing product functionality to historic failures to improve failure analysis in design. Research in Engineering Design, 16(1-2), 96–108.
Tumer, I. Y., & Smidts, C. S. (2011). Integrated design-stage failure analysis of software-driven hardware systems. Computers, IEEE Transactions on, 60(8), 1072–1084.
Tumer, I. Y., Stone, R. B., & Bell, D. G. (2003). Requirements for a failure mode taxonomy for use in conceptual design. In Proceedings of the international conference on engineering design, iced (Vol. 3).
Wiese, P. R., & John, P. (2003). Engineering design in the multi-discipline era: A systems approach. Wiley.
Zio, E. (2009). Reliability engineering: Old problems and new challenges. Reliability Engineering & System Safety, 94(2), 125–141.
The Prognostic and Health Management Society advocates open-access to scientific data and uses a Creative Commons license for publishing and distributing any papers. A Creative Commons license does not relinquish the author’s copyright; rather it allows them to share some of their rights with any member of the public under certain conditions whilst enjoying full legal protection. By submitting an article to the International Conference of the Prognostics and Health Management Society, the authors agree to be bound by the associated terms and conditions including the following:
As the author, you retain the copyright to your Work. By submitting your Work, you are granting anybody the right to copy, distribute and transmit your Work and to adapt your Work with proper attribution under the terms of the Creative Commons Attribution 3.0 United States license. You assign rights to the Prognostics and Health Management Society to publish and disseminate your Work through electronic and print media if it is accepted for publication. A license note citing the Creative Commons Attribution 3.0 United States License as shown below needs to be placed in the footnote on the first page of the article.
First Author et al. This is an open-access article distributed under the terms of the Creative Commons Attribution 3.0 United States License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.