{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:57:48Z","timestamp":1694624268203},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"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":[[2005,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We study the formal verification of programs written in\n            <jats:sub>d<\/jats:sub>\n            SL, an extension of the standard ST language used to program industrial controllers. It proposes a trade off between industrial and formal verification worlds. The main advantage of\n            <jats:sub>d<\/jats:sub>\n            SL is to provide a transparent code distribution through low level communication mechanisms. The behavior of the synthesized distributed system can therefore be formally modeled, easily monitored and formally verified. The verification of a\n            <jats:sub>d<\/jats:sub>\n            SL program, realized with the\n            <jats:italic>Spin<\/jats:italic>\n            tool, is eased by the definition of a lattice of models linked with a simulation relation preserving next-free LTL formulae. We show that, although\n            <jats:sub>d<\/jats:sub>\n            SL is an industrial programming language, it gives the possibility to verify systems designed with it. We illustrate the benefit of our approach with a simple control system of two canal locks.\n          <\/jats:p>","DOI":"10.1007\/s00165-005-0066-9","type":"journal-article","created":{"date-parts":[[2005,6,28]],"date-time":"2005-06-28T09:21:11Z","timestamp":1119950471000},"page":"177-200","source":"Crossref","is-referenced-by-count":6,"title":["The formal design of distributed controllers with\n            <sub>d<\/sub>\n            SL and Spin"],"prefix":"10.1145","volume":"17","author":[{"given":"Bram De","family":"Wachter","sequence":"first","affiliation":[{"name":"Computer Science Department, Universit\u00e9 Libre de Bruxelles, ULB CP212, boulevard du Triomphe, 1050, Bruxelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Genon","sequence":"additional","affiliation":[{"name":"Computer Science Department, Universit\u00e9 Libre de Bruxelles, ULB CP212, boulevard du Triomphe, 1050, Bruxelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Massart","sequence":"additional","affiliation":[{"name":"Computer Science Department, Universit\u00e9 Libre de Bruxelles, ULB CP212, boulevard du Triomphe, 1050, Bruxelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9dric","family":"Meuter","sequence":"additional","affiliation":[{"name":"Computer Science Department, Universit\u00e9 Libre de Bruxelles, ULB CP212, boulevard du Triomphe, 1050, Bruxelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"The B-book: assigning programs to meanings. ISBN 0-521-49619-5","author":"Abr J-R","year":"1996"},{"key":"p_2","volume-title":"IFSIC","author":"Aub P","year":"1997"},{"key":"p_3","doi-asserted-by":"crossref","first-page":"1270","DOI":"10.1109\/5.97297","article-title":"The synchronous approach to reactive and real-time systems. In","volume":"79","author":"Benveniste A","year":"1991","journal-title":"Proceedings of the IEEE"},{"key":"p_4","first-page":"11","volume-title":"Ritter GX (ed) Information Processing 89","author":"Ber G","year":"1989"},{"issue":"2","key":"p_5","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The esterel synchronous programming language: design, semantics, implementation","volume":"19","author":"Berry G","year":"1992","journal-title":"Sci Comput Program"},{"key":"p_6","first-page":"2","article-title":"Functionality decomposition by compositional correctness preserving transformation","volume":"13","author":"Brinksma H","year":"1995","journal-title":"South African Comput J"},{"key":"p_7","volume-title":"IEC 1131-3 programming methodology. Software engineering methods for industrial automated systems. ISBN 2-9511585-0-5. CJ International Editions","author":"Bonfattti F","year":"1997"},{"key":"p_8","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-46691-6_17","volume-title":"Foundations of software technology and theoretical computer science","author":"Castellani I","year":"1999"},{"key":"p_9","volume-title":"Conf Rec 14th Ann ACM Symp on Princ Prog Langs","author":"Caspi P","year":"1987"},{"key":"p_11","first-page":"132","volume-title":"Principles of distributed systems: 7th international conference, vol 3114 of LNCS","author":"De B","year":"2003"},{"issue":"4","key":"p_12","doi-asserted-by":"crossref","first-page":"864","DOI":"10.1137\/S0097539792225297","article-title":"The complexity of multiterminal cuts","volume":"23","author":"Dahlhaus E","year":"1994","journal-title":"SIAM J Comput"},{"key":"p_13","first-page":"3","volume-title":"IEEE computer society technical committe on operating systems and application environments newsletter, vol 4","author":"Esk M","year":"1990"},{"key":"p_14","volume-title":"U.L.B.","author":"Gen A","year":"2004"},{"key":"p_15","volume-title":"INPG","author":"Gir A","year":"1994"},{"issue":"3","key":"p_16","first-page":"418","article-title":"Cache-coherent distributed shared memory: perspectives on its development and future challenges","volume":"87","author":"Hennessy J","year":"1999","journal-title":"Proc IEEE Spec Issue Distrib Shared Mem"},{"key":"p_17","volume-title":"The spin model checker - primer and reference manual","author":"Hol GJ","year":"2003"},{"key":"p_18","first-page":"474","volume-title":"Proceedings: 9th International conference on high performance computing","author":"Jiang H","year":"2002"},{"key":"p_19","volume-title":"Parallel program design: a foundation","author":"Misra J","year":"1988"},{"issue":"9","key":"p_20","doi-asserted-by":"crossref","first-page":"1321","DOI":"10.1109\/5.97301","article-title":"Programming real time applications with signal","volume":"79","author":"LeGuernic P","year":"1991","journal-title":"Proc IEEE"},{"key":"p_21","volume-title":"Proceedings of the 10th international conference, TACAS 2004, vol 2988 of LNCS, pp 327-341. ETAPS 2004, Springer, Berlin Heidelberg New York","author":"Leue S","year":"2004"},{"key":"p_22","first-page":"281","volume-title":"Proceedings of the FORTE'91 conference","author":"Mas T","year":"1992"},{"key":"p_24","volume-title":"Communication and concurrency. PHI Series in Computer Science","author":"Mil R","year":"1989"},{"key":"p_25","first-page":"549","volume-title":"Proceedings of the CONCUR'98","author":"Mor R","year":"1999"},{"issue":"9","key":"p_26","doi-asserted-by":"crossref","first-page":"959","DOI":"10.1109\/71.615441","article-title":"A survey of recoverable distributed shared memory systems","volume":"8","author":"Morin C","year":"1997","journal-title":"IEEE Trans Parallel Distributed Syst"},{"issue":"8","key":"p_27","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/2.84877","article-title":"Distributed shared memory: a survey of issues and algorithms","volume":"24","author":"Nizeberg B","year":"1991","journal-title":"IEEE Comput"},{"key":"p_28","first-page":"27","volume-title":"Proceedings of the 14th International conference on concurrency theory (CONCUR'03)","author":"Stefanescu A","year":"2003"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0066-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0066-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0066-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:53:05Z","timestamp":1641484385000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0066-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["10.1007\/s00165-005-0066-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0066-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,8]]}}}