{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:17Z","timestamp":1761611177026},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2001,9]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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 (LOTOS) is automatic from the definition of architectural operators.<\/jats:p>","DOI":"10.1007\/pl00003939","type":"journal-article","created":{"date-parts":[[2006,4,10]],"date-time":"2006-04-10T10:57:22Z","timestamp":1144666642000},"page":"50-91","source":"Crossref","is-referenced-by-count":33,"title":["SCTL-MUS: A Formal Methodology for Software Development of Distributed Systems. A Case Study"],"prefix":"10.1145","volume":"13","author":[{"given":"Jos\u00e9 J.","family":"Pazos Arias","sequence":"first","affiliation":[{"name":"\u00c1rea de Ingenier\u00eda Telem\u00e1tica, University of Vigo, Spain, , , , , , ES"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge Garc\u00eda","family":"Duque","sequence":"additional","affiliation":[{"name":"\u00c1rea de Ingenier\u00eda Telem\u00e1tica, University of Vigo, Spain, , , , , , ES"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"4","key":"p_1","first-page":"34","article-title":"Monterey Workshop, Monterey, CA, 1994. [BuF96] Burke, E. and Foxley, E.: Logic and its Applications. Prentice Hall, Englewood Cliffs, NJ, 1996. [BoH95a] Bowen, J. P. and Hinchey, M. G.: Seven more myths of formal methods","volume":"12","author":"Ber","year":"1994","journal-title":"IEEE Software"},{"key":"p_2","volume-title":"Application and Tools","author":"Formal Description Techniques IX."},{"key":"p_3","first-page":"95","volume-title":"A. P.: Automatic verification of finite-state concurrent systems using temporal","author":"Chapman"},{"key":"p_4","volume-title":"ACM Transactions on Programming Languages and Systems, 8(2):244-263","year":"1986"},{"key":"p_5","unstructured":"Languages 1992. [ChJ90] Cheng J. H. and Jones C. B.: On the usability of logics which handle partial functions. In C. Morgan and J. Woodcock"},{"key":"p_6","volume-title":"Proceedings of the Third Refinement Workshop. Springer","year":"1990"},{"issue":"4","key":"p_7","first-page":"16","article-title":"[Dav93] Davis, A. M.: Software Requirements: Objects, Functions and States. Prentice-Hall, Englewood Cliffs, NJ, 1993. [DiR96] Dill, D. L. and Rushby, J.: Acceptance of formal methods: lessons from hardware design","volume":"29","author":"Surveys","year":"1996","journal-title":"IEEE Computer"},{"key":"p_8","volume-title":"Ed. Revert\u00e9","author":"Fe","year":"1994"},{"key":"p_9","volume-title":"IEE\/BCS Software Engineering Journal","author":"Communications ACM","year":"1994"},{"key":"p_10","first-page":"203","article-title":"[Got92] Gotzhein, R.: Temporal logic and its applications","volume":"24","author":"Ph","year":"2000","journal-title":"Computer Networks and ISDN Systems"},{"issue":"5","key":"p_11","first-page":"11","article-title":"[Hal90] Hall, J. A.: Seven myths of formal methods","volume":"7","author":"Englewood Cliffs NJ.","year":"1996","journal-title":"IEEE Software"},{"key":"p_12","unstructured":"21(3):251-269 1984. [HaJ89] Hayes I. J. and Jones C. B.: Specifications are not (necessarily) executable. IEE\/BCS Software Engineering Journal"},{"key":"p_13","unstructured":"4(6):320-338 1989."},{"key":"p_38","unstructured":"If I[1] = \u2191 return cardinal = 1;"},{"key":"p_39","volume-title":"return cardinal = 3","author":"If"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/PL00003939.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/PL00003939\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/PL00003939","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:36:27Z","timestamp":1641483387000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/PL00003939"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,9]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,9]]}},"alternative-id":["10.1007\/PL00003939"],"URL":"https:\/\/doi.org\/10.1007\/pl00003939","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,9]]}}}