Formal techniques have been shown to be useful in the development of correct software. But the level of expertise required of practitioners of these techniques prohibits their widespread adoption. Attempts to integrate formal specification techniques with modern, often agile, software development practices are becoming more successful. However, these new techniques do not yet have development environments that facilitate the construction of consistent specifications for the non-expert developer. :Many of the tools that support the analysis of specifications expressed in these languages give misleading feedback in cases where the specification is inconsistent. Further, logical changes made to a specification typically invalidate the results of previous analyses. This thesis is therefore concerned with the development of an environment to facilitate the construction of correct specifications. Analysis patterns are identified that guide a non-expert specifier through some of the logical pitfalls of analysing a program specification. A change management framework for program specifications is described, which minimises the number of SAT calls needed to recheck the consistency of an edited specification. A lightweight program specification language, called Loy, is defined, which can be automatically analysed by the Alloy Analyzer, through a formal encoding of Loy into Alloy. A prototype tool is presented that automates the encoding and implements the analysis patterns and change management framework in the context of Loy specifications.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:506765 |
| Date | January 2008 |
| Creators | Heaven, William John Douglas |
| Publisher | Imperial College London |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0379 seconds