×

SCTL-MUS

swMATH ID: 2245
Software Authors: Pazos Arias, José J.; García Duque, Jorge
Description: SCTL-MUS: A formal methodology for software development of distributed systems. A case study This paper introduces an iterative model for the software development process of distributed systems. It is based on dealing with the system evolution and maintenance activities as similar stages of the system development. In order to formalise this model, a multi-valued causal temporal logic, referred to as Simple Causal Temporal Logic (SCTL), is defined for the acquisition and specification of the functional requirements. A Model of Unspecified States (MUS) is also defined with a double goal: firstly, to show the fundamental aspects of system behaviour, which has been specified through a set of SCTL requirements; and, secondly, to verify the consistency and completeness of the specified requirements.par The combination of SCTL and MUS allows obtaining the specification of the initial architecture of the system formally. Besides, the design decisions are stored with the goal of making the evolution and maintenance tasks easier. The translation between MUS and a constructive formal description technique is automatic from the definition of architectural operators.
Homepage: http://rd.springer.com/article/10.1007/PL00003939
Keywords: simple causal temporal logic; model of unspecified states
Related Software: PVS; NuSMV; SLAM; TLA
Cited in: 5 Publications

Citations by Year