Reusability of Modeling and Verification Components between the DesignBIP and FSolidM Design Studios
Authors: Anastasia Mavridou1, Aron Laszka2, and Janos Sztipanovits1
1Vanderbilt University and 2University of Houston
Abstract
Design studios facilitate system development by providing system architects with all necessary tools and services for modeling, verifying, and generating systems. Design studio components can be organized in three main categories: 1) semantic integration, 2) service integration, and 3) tool integration components. Semantic integration components comprise the domain of the modeling language, i.e., its metamodel, which explicitly specifies the building blocks of the language and their relations. Service integration components include dedicated model editors, code editors, and components for visualization of simulation and verification results. Additionally, service integration components include model transformation and code generation services, consistency and type checking mechanisms, model repositories, and version control services. Finally, tool integration components consist of interfaces and integration services towards integrated tools, such as simulation and verification tools.
We have developed two design studios: 1) the DesignBIP studio for modeling, verifying, and generating systems using the Behavior-Interaction-Priority (BIP) component-based framework and 2) the FSolidM studio for designing, verifying, and generating secure Solidity smart contracts for Ethereum blockchains. We have reused several components between the two design studios, such as model editors and integrated verification tools. In particular, the modeling languages that describe the behavior of DesignBIP models and FSolidM smart contracts are both based on Finite State Machines (FSM), which allowed us to reuse the FSM-based model editor. To verify the correctness of smart contracts, we have used BIP. To do that, we have defined an equivalent transformation from FSolidM FSMs to BIP FSMs and implemented it as a plugin in FSolidM. Additionally, we have integrated a tool in both design studios that transforms BIP models into observationally equivalent SMV models, which is the input language of the NuSMV model checker. To verify the correctness of BIP and FSolidM models, we have integrated into both design studios the NuSMV model checker and simulation tools from the BIP toolset.
We present the design flow of both studios, which is as follows. Initially, models are designed using dedicated model editors. Optionally, safety and security patterns can be used to simplify the modeling process by adding useful functionality or by enforcing important safety and security properties by construction. Next, the checking loop starts in which the models are checked for conformance. Additionally, the models can be checked for safety and liveness properties, as well as deadlock freedom using the integrated NuSMV model checker and BIP simulation tools. If the required conformance conditions are not satisfied by the model, then the design studio informs the user of the problematic nodes of the model and of the inconsistency causes to facilitate model refinement. Similarly, if the required safety/liveness properties are not satisfied by the model, the design studio returns counterexamples based on faulty execution paths. Finally, when the conformance conditions and safety/liveness properties are satisfied, the code (Java for DesignBIP and Solidity for FSolidM) may be generated.