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 &#8216;bug&#8217; 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

   * [[Alloy]]