A JML-Based strategy for incorporating formal specifications into the software development process

Pestana, João Miguel Alves

http://hdl.handle.net/10400.13/78

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
MestradoJoaoPestana.pdf		883.25 KB	Adobe PDF	Download

Send Feedback

Authors

Pestana, João Miguel Alves

Abstract(s)

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.

Keywords

Software development Software correctness Formal methods Design by contract Java Modelling Language (JML) JML-based strategy Informal functional requirements Semi-formal functional requirements Invariants Formal specifications Abstract variables Java . Centro de Ciências Exatas e da Engenharia