X-MAN System modelling and verification through automated theorem proving

Abstract

Component-Based Development (CBD) is a promising software development paradigm claiming development of cost-effective, highly productive, and time-saving software systems. Constructing a large and complex software system under CBD demands a hierarchically compositional structure of components that meets both functional and non-functional requirements of a system along with newly faced challenges of CBD, which are scalability, complexity and safety. Currently, there are a number of component models available which are practiced throughout the CBD community. Unfortunately, they present different views of a component model and due to this, most of them are using components which are tightly coupled and hierarchically non-compositional in nature.In contrast, X-MAN component model uses encapsulated components and exogenous composition connectors which makes them loosely-coupled and hierarchically composable in nature.In order to check the correctness of these connectors and how they support hierarchical system constructionto meet new challenges, a 3 step formal verification approach is followed. Using a graphical representation in High Level Petri Net (HLPN) model and Z specification language for specifying transition rules, a number of properties are asserted which are verified by the Z3 automated theorem prover.