Home
Links
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
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 * [[Alloy]]