Skip to main content

Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering

Leonardo Mangeruca

The complexity of modern aircraft development is rising constantly pushed by the growth of thetransportation market, the continuous technology improvements, the rising of new technologies, thedevelopment of more challenging regulations and the ever increasing competition. The high costinvestments involved with the development of an aircraft and its constituent systems leads airframers andsystem suppliers to take critical design decisions early, with a potentially high risk on the development andoperational costs of the aircraft. On the other hand, the increasing complexity makes the costs and risksconnected with the verification and testing of aircraft systems and their integration constantly rising.These considerations are pushing the aerospace industry towards growing deployment of model-basedmethods to anticipate design problems closer in time to when the design decisions are taken, to reduce therisk of turn-backs and migrate towards a virtual testing driven development process to gradually achieveright-the-first-time test rig campaigns and safety-of-flight.In this evolving landscape, promising model-based technologies beyond simulation are emerging to supportthis view, including property falsification, automatic test generation and coverage and formal verificationtechnologies. Nonetheless, there still remain compelling challenges to overcome to render thesetechnologies widely applicable across the aerospace industry. In this paper, we present such challenges andposition them in context of the development process of aerospace systems and relevant aerospaceengineering standards.

Speaker bio

Leonardo Mangeruca is serving as Group Leader for the System Analysis, Control and Optimization group at UTRC – United Technologies Research Center, providing technical leadership to advance UTRC capabilities for system analysis, control and optimization. Leonardo has provided key contributions in several formal verification and system simulation technologies to enable successful industrial deployment of advanced state-of-the-art methods at UTC – United Technologies Corporation, designing and developing technology enhancements, novel modeling techniques, application methodologies and processes. Leonardo received his PhD degree and Dr. Eng. degree in Electrical Engineering and Computer Science from the University of Genova, Italy and was intern at Cadence Berkeley Laboratories. He took part in several European projects collaborating with leading academic and industrial European institutions. He published numerous papers in conference proceedings and international journals in the areas of model-based design and formal verification of embedded systems and real-time systems analysis and co-authored two patents in the area of safety-critical micro-controllers.

Share this: