*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Aroua Gharbi
(Advisor: Prof. Dimitri Mavris)
will defend a doctoral thesis entitled,
Toward A Robust Computational Solution for Formal Verification and Validation in Model-Based Systems Engineering
On
Thursday, April 14 at 9:00 a.m.
Collaborative Visualization Environment (CoVE)
Weber Space Science and Technology Building (SST II)
And
https://bluejeans.com/228679479/0542
Abstract
The development of reliable, large complex systems relies on a systematic approach with well-established standards and practices. One of these standards is Model-Based Systems Engineering (MBSE), which adopts an approach that centers models to design, analyze and maintain products throughout their life cycle. To maximize the quality and output of these models, multiple verification and validation activities need to be conducted throughout this process. Despite numerous advances, these activities are time-consuming, primarily based on heuristics, and performed in a bottom-up approach that assumes that the validity of subsystems guarantees the correctness of their composite model.
Popularized in the 1960s, formal methods rectify the shortcomings of heuristic approaches by using mathematics to provide proof of correctness. Formal verification and validation (V&V) are heavily used in software design and engineering to help generate correct codes and identify unforeseen situations. Formal V&V techniques used in MBSE are extrapolated from software engineering practices. They center on model checking, which is a form of verification only. Therefore, a new approach to formal verification and validation in MBSE needs to stem from the characteristics of the discipline itself.
A couple of authors attempted to provide a rigorous foundation of MBSE. The most notable and comprehensive one is the Tricotyledon Theory of System Design (T3SD), developed by Wayne Wymore in 1993. Founded on the set theory, T3SD laid the groundwork for a system design language to rigorously solve design engineering problems. Wymore was the first to coin the term MBSE and establish the tools and mechanisms to adopt it in a design process. However, this theory was a victim of its rigor and exhaustiveness as the complexity of its mathematical constructs deterred practitioners from using it. For almost 30 years, all the concepts, problems, and examples developed by Wymore remained as an abstract proof in his book. Yet, T3SD has the mathematical formalism needed to create a robust verification and validation framework. For instance, the System Design Problem (SDR) provides a concise formulation of the MBSE design problem from which proof-based assertions can be deduced. In this thesis, a methodology is proposed to (1) provide computational implementations to the complex constructs of T3SD and (2) generate an algorithmic solution to SDR.
In the first step of the proposed methodology, the theory elements are arranged hierarchically based on their inter-dependency. Next, the SDR statement is decoupled, leading to the identification of practical phases for a formal verification and validation task. These phases are centered on two critical T3SD concepts: the System Coupling Recipe (SCR), which is concerned with the structural composition of systems, and system homomorphisms, a mathematical tool to identify the equivalence between systems.
To provide a computational implementation of SCR, Wymore’s state transition diagrams were proved to be a special case of Finite-State Machines (FSM). As FSMs are mathematical models of computation, in essence, an algorithm was developed to support a code that calculates the resultant of a SCR. The correctness of this implementation was demonstrated in multiple examples as part of this thesis.
For the concept of system homomorphisms, its T3SD definition was reformulated using mathematical logic. The new formulation resulted in an instance of the satisfiability problem (SAT), for which a Python code using the Gurobi optimizer was developed. The correctness of the reformulation and implementation were also validated and demonstrated in examples in this thesis. Finally, a holistic postulate for SDR was concluded. This postulate proposed a many-objective ordering solution of partially ordered sets (posets) for the formal approach to verification and validation. Aside from being the first extensive investigation of T3SD, the methodology developed as part of this research represents a first down-payment toward a practical computational solution for formal verification and validation in MBSE. The algorithms and codes developed in this thesis enable a set-up of real-life design problems, where the conformance between a candidate solution and its requirements can be established objectively.
Committee
