Comparative Assessment of System Description Methodologies and FormalSpecification Languages

摘要

A classification of formal specification techniques which is useful for thecomparative assessment of computer systems is presented. In this classification, formal specification techniques are grouped into three approaches; operational, definitional and hybrid. Depending on whether data abstraction or sequencing is emphasized, the operational and definitional approaches both can be further partitioned into two schools: data paradigm and process paradigm. Five categories are identified, and some representative formal specification techniques in each category are surveyed. A comparative assessment over these specification techniques is given based on a set of criteria, such as usability, verifiability, support for nonfunctional requirements, etc. Our experience in using formal specification techniques are discussed. A real time extension of the VDM method, designated RT-VDM, is presented as the most promising approach for further study. Additional recommendations for further study are also made.