{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T22:51:18Z","timestamp":1761519078259,"version":"3.41.2"},"reference-count":30,"publisher":"SAGE Publications","issue":"8","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["International Journal of Advanced Robotic Systems"],"published-print":{"date-parts":[[2013,8,1]]},"abstract":"<jats:p> As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics used to express the properties of a system's behaviour is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process. Errors in this step of the process can create serious problems since a false sense of safety is gained from the analysis. However, when compared to the effort put into developing and applying modelling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. In this paper we illustrate how a collection of property patterns can help in simplifying the process of generating logical formulae from informally expressed requirements. <\/jats:p>","DOI":"10.5772\/56412","type":"journal-article","created":{"date-parts":[[2013,8,30]],"date-time":"2013-08-30T13:35:10Z","timestamp":1377869710000},"update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":8,"title":["A Specification Patterns System for Discrete Event Systems Analysis"],"prefix":"10.1177","volume":"10","author":[{"given":"Jose Creissac","family":"Campos","sequence":"first","affiliation":[{"name":"Departamento de Informatica\/Universidade do Minho & HASLab\/INESC TEC, Portugal"}]},{"given":"Jose","family":"Machado","sequence":"additional","affiliation":[{"name":"Departamento de Engenharia Mecanica\/CT2M, Universidade do Minho, Portugal"}]}],"member":"179","published-online":{"date-parts":[[2013,1,1]]},"reference":[{"key":"bibr1-56412","doi-asserted-by":"publisher","DOI":"10.1109\/37.272781"},{"key":"bibr2-56412","first-page":"905","volume":"36","author":"Roussel J. M.","year":"2002","journal-title":"Journal Europ\u00e9en des Syst\u00e9mes Automatis\u00e9s"},{"key":"bibr3-56412","doi-asserted-by":"crossref","unstructured":"De Smet O.,  and Rossi O. Verification of a controller for a flexible manufacturing line written in Ladder Diagram via model-checking. In 21th American Control Conference, ACC'02: 4147\u20134152, Anchorage, USA, May 2002. CDROM paper n. 734, 2002.","DOI":"10.1109\/ACC.2002.1024580"},{"key":"bibr4-56412","unstructured":"Rossi O. Validation formelle de programmes ladder pour automates programmables industriels. PhD thesis, \u00c9cole Normale Sup\u00e9rieure de Cachan, France, 2003."},{"key":"bibr5-56412","doi-asserted-by":"publisher","DOI":"10.3166\/jesa.39.1079-1098"},{"key":"bibr6-56412","doi-asserted-by":"crossref","unstructured":"Machado J., Denis B.,  and Lesage J. J. A generic approach to build plant models for DES verification purposes. In 8th International Workshop On Discrete Event Systems (WODES'06): 407\u2013412, 2006.","DOI":"10.1109\/WODES.2006.382508"},{"volume-title":"Systems and Software Verification: Model-Checking techniques and tools","year":"1999","author":"B\u00e9rard B.","key":"bibr7-56412"},{"volume-title":"Verification of sequential function charts using SMV In International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 2000), V: 987\u20132993","year":"2000","author":"Bornot S.","key":"bibr8-56412"},{"key":"bibr9-56412","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"volume-title":"Proceedings of the 17th IFAC World Congress: 5107\u20135112","year":"2008","author":"Campos J. C.","key":"bibr10-56412"},{"volume-title":"Compositionality: The Significant Difference, Volume 1536 of Lecture Notes in Computer Science","year":"1998","author":"de Roever W. P.","key":"bibr11-56412"},{"key":"bibr12-56412","doi-asserted-by":"crossref","unstructured":"Frey G.,  and Litz L. Formal method in PLC programming. In IEEE Int. Conf. on Systems, Man and Cybernetics: 2431\u20132436, 2000.","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"bibr13-56412","doi-asserted-by":"crossref","unstructured":"Lamp\u00e9ri\u00e8re-Couffin S., Rossi O., Roussel J.M.,  and Lesage J.J. Formal validation of PLC programs: A survey. In Proceedings of the ECC'99: European Control Conference, 1999.","DOI":"10.23919\/ECC.1999.7099641"},{"key":"bibr14-56412","doi-asserted-by":"publisher","DOI":"10.1016\/0360-8352(95)00159-X"},{"key":"bibr15-56412","doi-asserted-by":"publisher","DOI":"10.1016\/S0360-8352(96)00216-1"},{"key":"bibr16-56412","doi-asserted-by":"crossref","unstructured":"Rausch M.,  and Krogh B. H. Formal verification of PLC programs. In Proceedings of the American Control Conference: 234\u2013238, 1998.","DOI":"10.1109\/ACC.1998.694666"},{"key":"bibr17-56412","first-page":"65","author":"Hassapis G.","year":"1998","journal-title":"Proceedings of INCOM'98"},{"key":"bibr18-56412","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2001.972974"},{"key":"bibr19-56412","unstructured":"Rossi O. Validation formelle de programmes ladder pour automates programmables industriels. PhD thesis, \u00c9cole Normale Sup\u00e9rieure de Cachan, France, 2004."},{"key":"bibr20-56412","doi-asserted-by":"crossref","unstructured":"Canet G., Couffin S., Lesage J. J., Petit A.,  and Schnoebelen P. Towards automatic verification of PLC programs written in Instruction List. In IEEE Int Conf. on Systems, Man and Cybernetics: 2449\u20132454, 2000.","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"bibr21-56412","doi-asserted-by":"crossref","unstructured":"Kowalewski S.,  and Preu\u00dfig J. Verification of sequential controllers with timing functions for chemical processes. In 13th IFAC World Congress, invited session on Advances in Discrete Event Control, 1996.","DOI":"10.1016\/S1474-6670(17)58447-5"},{"key":"bibr22-56412","first-page":"751","volume":"7","author":"Zaytoon J.","year":"1999","journal-title":"APII \u2013 Journal Europ\u00e9en des Syst\u00e8mes Automatis\u00e9s"},{"volume-title":"Temporal Verification of Reactive Systems: Specification","year":"1991","author":"Manna Z.","key":"bibr23-56412"},{"key":"bibr24-56412","doi-asserted-by":"publisher","DOI":"10.21236\/ADA227320"},{"volume-title":"Addison-Wesley Professional Computing Series","year":"1995","author":"Gamma E.","key":"bibr25-56412"},{"key":"bibr26-56412","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"bibr27-56412","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-4230(01)00014-6"},{"volume-title":"Automatic verification of temporal and timed properties of control programs","year":"2004","author":"Zoubek B.","key":"bibr28-56412"},{"key":"bibr29-56412","doi-asserted-by":"publisher","DOI":"10.1016\/S0098-1354(01)00656-1"},{"volume-title":"Influence de la prise en compte d'un mod\u00e8le de processus en v\u00e9rification formelle des Syst\u00e8mes \u00e0 Ev\u00e9nements Discrets","year":"2006","author":"Machado J. M.","key":"bibr30-56412"}],"container-title":["International Journal of Advanced Robotic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.5772\/56412","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.5772\/56412","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.5772\/56412","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,10]],"date-time":"2025-03-10T21:58:35Z","timestamp":1741643915000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.5772\/56412"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,1]]},"references-count":30,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2013,8,1]]}},"alternative-id":["10.5772\/56412"],"URL":"https:\/\/doi.org\/10.5772\/56412","relation":{},"ISSN":["1729-8806","1729-8814"],"issn-type":[{"type":"print","value":"1729-8806"},{"type":"electronic","value":"1729-8814"}],"subject":[],"published":{"date-parts":[[2013,1,1]]},"article-number":"315"}}