Formal Verification of Complex Systems based on SysML Functional Requirements



Published Sep 29, 2014
Hoda Mehrpouyan Irem Y. Tumer Chris Hoyle Dimitra Giannakopoulou Guillaume Brat


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

Mehrpouyan, H. ., Y. Tumer, I. ., Hoyle, C. ., Giannakopoulou, D., & Brat, G. . (2014). Formal Verification of Complex Systems based on SysML Functional Requirements. Annual Conference of the PHM Society, 6(1).
Abstract 205 | PDF Downloads 147



early system design, failure prognosis, Verification, safety analysis

ARP4754, S. (1996). Certification considerations for highly- integrated or complex aircraft systems. Society of Automotive Engineers Inc.

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. 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-

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.
Technical Research Papers