Bi-directional Consistency Checking Based On Temporal Logic

Nowadays, formal method is one of the important way to build credible software systems. When handling development driven formal models, the developers have to build a formal model, verify it and then writing the codes corresponding to the verified model. Current techniques cannot generate the codes from the model totally automatically. There will surely remain some codes that is required to write by the developers manually, so it is important to keep consistency checking throughout the developing process. Under ideal conditions, the developers need only to accomplish model-based testing to ensure the codes are consistent with the model.However, growing with the complexity of software systems and the frequency of requirements changing, maintaining the consistency between software models and their implementation becomes more and more challengeable. While traditional model-based testing focuses on ensuring the software implementation comply with its designed model, there exist situations that the implementation is modified while software models are left outdated. Reverse engineering, workarounds during deployment, key component verification after the codes have done are examples in point. The model designers have to manually assert the consistency between model and codes, which greatly reduce the effectiveness and system reliability.Thus, this paper presents an automated consistency checking framework, which extends traditional model-based testing with mining software properties represented as temporal logic formulas for identified inconsistencies. The generated temporal logic formulas can help to automatically check the consistency for the model with model checkers when model designers are trying to fix the inconsistency.Meanwhile, this paper introduce one implementation of the bi-way consistency checking framework above called:ProMiner. ProMiner is built basing on formal modeling language Event-B’s open source IDE Rodin, and is published as a plugin for Rodin. ProMiner can generate linear temporal logic formulars (LTL) and integrate ProB for model checking. It also have the ability to support model-based testing and LTL translation or optimization. Experiments show that ProB can effectively help software designer to narrow down the specific locations of software models that need to be updated with respects to its running implementation.