Loading...
Please wait, while we are loading the content...
Similar Documents
Development of Verifiable Programs-Application of an Approach based on Executable Object-Oriented Specifications
| Content Provider | Semantic Scholar |
|---|---|
| Author | Sharygina, Natasha Browne, James C. Tesar, Delbert |
| Copyright Year | 2001 |
| Abstract | Combining validation by testing with verification by formal methods offers great potential for development of robust and reliable object-oriented software systems. However, formal verification cannot be readily applied to software developed with conventional object-oriented development methods. This paper presents the first phase of a two-phase approach for development of object-oriented software systems which combines validation of OOA models formulated in xUML (an executable subset of UML[18],[24]) with formal verification through model checking. The second phase, application of model checking to the validated OOA model has been presented separately [22]. Model checking is accomplished by translating the validated OOA model to the COSPAN, automaton-based model checking system [5]. This paper defines, describes and illustrates an OOA model construction process leading to OOA models which can be both validated and verified. This process leads to efficient designs, which minimizes complexity of the resulting computer-controlled systems. Since OOA models in xUML are executable they can be validated by testing using simulation. Finally, since the OOA model complexity level is much less than the procedural programs to which they are translated, model-checking can be applied to the validated OOA model. We demonstrate the approach by applying it to reengineering of a NASA robotic system where testing and maintenance had been obstructed by complexity. A comparative analysis between the original robotic system, that was constructed following the Booch methodology [1], and the redesigned system is given. A number of inefficiencies and flaws in the original design which would have precluded model checking were found. An OOA model to which model checking has been successfully applied resulted from the redesign. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.utexas.edu/ftp/techreports/tr02-16.pdf |
| Alternate Webpage(s) | http://www.cs.cmu.edu/~natalie/Publications/tr02-16.pdf |
| Alternate Webpage(s) | http://www.cs.utexas.edu/ftp/pub/techreports/tr02-16.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
