SCTL-MUS

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.


References in zbMATH (referenced in 8 articles , 1 standard article )

Showing results 1 to 8 of 8.
Sorted by year (citations)

  1. García-Duque, Jorge; Pazos-Arias, José J.; López-Nores, Martín; Blanco-Fernández, Yolanda; Fernández-Vilas, Ana; Díaz-Redondo, Rebeca P.; Ramos-Cabrer, Manuel; Gil-Solla, Alberto: Methodologies to evolve formal specifications through refinement and retrenchment in an analysis-revision cycle (2009)
  2. Barragáns Martínez, Ana Belén; Pazos Arias, José J.; Fernández Vilas, Ana; García Duque, Jorge; López Nores, Martín; Díaz Redondo, Rebeca P.; Blanco Fernández, Yolanda: Composing requirements specifications from multiple prioritized sources (2008)
  3. Chechik, Marsha; Gurfinkel, Arie; Devereux, Benet; Lai, Albert; Easterbrook, Steve: Data structures for symbolic multi-valued model-checking (2006)
  4. García-Duque, Jorge; López-Nores, Martín; Pazos-Arias, José J.; Fernández-Vilas, Ana; Díaz-Redondo, Rebeca P.; Gil-Solla, Alberto; Blanco-Fernández, Yolanda; Ramos-Cabrer, Manuel: A six-valued logic to reason about uncertainty and inconsistency in requirements specifications (2006)
  5. García-Duque, Jorge; López-Nores, Martín; Pazos-Arias, José J.; Fernández-Vilas, Ana; Díaz-Redondo, Rebeca P.; Gil-Solla, Alberto; Ramos-Cabrer, Manuel; Blanco-Fernández, Yolanda: Guidelines for the incremental identification of aspects in requirements specifications (2006)
  6. Fernández Vilas, Ana; Pazos Arias, José J.; Díaz Redondo, Rebeca P.; Gil Solla, Alberto; García Duque, Jorge: A many-valued logic with imperative semantics for incremental specification of timed models (2004)
  7. Fernández Vilas, Ana; Pazos Arias, José J.; Díaz Redondo, Rebeca P.: Extending timed automaton and real-time logic to many-valued reasoning (2002)
  8. Pazos Arias, José J.; García Duque, Jorge: SCTL-MUS: A formal methodology for software development of distributed systems. A case study (2001)