Concept Paper AVOOM
FOO
An Approach To Verify Formal Object-Oriented Software Model
Abstract
This paper presents an early idea of verifying a formal object-oriented software model. In general, the input to verification process is the model and the properties that we want to check. In this paper, the software model will be represented in Object-Z. Whilst the properties will be translated as formulas. In order to check whether the model satisfy the properties, we will map the Object-Z model and its properties into Alloy. In particular the approach used by Alloy (
http://alloy.mit.edu) is interesting. Alloy is a constraint solver. We can write models (of software) and properties, acting as constraints. These are converted to formulas. A backend SAT solver tries to find a bounded model satisfying the formulas. Like model checkers, SAT is an automatic verification technology. This combination of SAT and model bounding is extremely effective for ‘bug’ hunting. Alloy has in addition the benefit of having a declarative modelling language. Historically it was also greatly influenced by Z.
Motivation
Modelling: Object-Z
Checking the models: Alloy
Conclusion and Future Work
Related Work
