Addressing the Construction of Z and Object-Z with Use Case Maps (UCMs)

作者：Dongmo Cyrille^*; van der Poll John Andrew

来源：International Journal of Software Engineering and Knowledge Engineering, 2014, 24(2): 285-327.

DOI：10.1142/S0218194014500120

• Requirements specification
• specification process
• constructivity UCM
• Z
• object-Z

A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from a set of use cases normally expressed in natural language. Natural languages are, however, inherently ambiguous and as a semi-formal notation, UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. The semi-formal notation of UCMs aims to show how things work generally, but is not suitable to reason formally about system behavior. It is plausible, therefore, that the use of a UCM as an intermediate step may facilitate the construction of a formal specification. To this end this paper proposes a mechanism whereby a UCM may be translated into Object-Z.

• 出版日期2014-3