{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T03:08:49Z","timestamp":1768273729359,"version":"3.49.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2004,8,1]],"date-time":"2004-08-01T00:00:00Z","timestamp":1091318400000},"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":[[2004,8]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            Semantics of description languages for complex systems are a central issue for implementing verification methods such as\n            <jats:italic>abstract model checking<\/jats:italic>\n            . This technique is employed to verify systems by inspecting only a small state space that represents its potential behaviors. This paper presents a generalized operational semantics of the modelling language promela that provides the theoretical basis to introduce this promising method in the model checker SPIN. The generalization consists of identifying language aspects affected by the abstraction. Using these aspects as parameters, it is possible to obtain and relate different interpretations of the language. The new semantics provides a framework to reason about how to construct the tool \u03b1spin as an extension of spin.\n          <\/jats:p>","DOI":"10.1007\/s00165-004-0040-y","type":"journal-article","created":{"date-parts":[[2004,5,19]],"date-time":"2004-05-19T05:48:45Z","timestamp":1084945725000},"page":"166-193","source":"Crossref","is-referenced-by-count":14,"title":["A generalized semantics of PROMELA for abstract model checking"],"prefix":"10.1145","volume":"16","author":[{"given":"Mar\u00eda del Mar","family":"Gallardo","sequence":"first","affiliation":[{"name":"Dpto. de Lenguajes y Ciencias de la Computaci\u00f3n, University of Malaga, 29071, Malaga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[{"name":"Dpto. de Lenguajes y Ciencias de la Computaci\u00f3n, University of Malaga, 29071, Malaga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernesto","family":"Pimentel","sequence":"additional","affiliation":[{"name":"Dpto. de Lenguajes y Ciencias de la Computaci\u00f3n, University of Malaga, 29071, Malaga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","first-page":"69","article-title":"A parameterized semantics for sequential function charts. In: the proceedings of SFEDL (Semantic Foundations of Engineering Design Languages)","volume":"2002","author":"Ba N","year":"2002","journal-title":"Satellite Event of ETAPS"},{"key":"p_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer aided verification, LNCS-1427","author":"Bensalem S","year":"1998"},{"key":"p_3","volume-title":"Proceedings of the third SPIN workshop, SPIN97","author":"Bev WR","year":"1997"},{"key":"p_4","volume-title":"ACM trans programming lang syst 8(2):244-263","author":"Clarke EM","year":"1986"},{"key":"p_5","volume-title":"ACM trans programming lang syst 16(5):1512-1542","author":"Clarke EM","year":"1994"},{"key":"p_6","volume-title":"Model checking","author":"Clarke E","year":"2000"},{"key":"p_7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01211314","article-title":"Testing equivalence as a bisimulation equivalence","volume":"5","author":"Cl R","year":"1993","journal-title":"Formal Aspects Comput"},{"key":"p_8","first-page":"39","volume-title":"Constraint processing, selected papers.","author":"Co C","year":"1995"},{"key":"p_9","first-page":"238","volume-title":"Proceedings of the conference record of the 4th ACM symposium on principles of programming languages.","author":"Co P","year":"1977"},{"key":"p_10","volume-title":"Abstract interpretation of reactive systems. ACM Trans programming lang syst 19(2):253-291","author":"Dams D","year":"1997"},{"key":"p_11","first-page":"187","volume-title":"SPIN model checking and software verification, LNCS-1885","author":"Fe E","year":"2000"},{"key":"p_12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-1998-341201","article-title":"Parameterized structured operational semantics","volume":"34","author":"Fe L","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"p_13","first-page":"184","volume-title":"LNCS-1680","author":"Ga MM","year":"1999"},{"key":"p_15","volume-title":"Proceedings of the 6th world conference on integrated design and process technology","author":"Gallardo MM","year":"2002"},{"key":"p_16","volume-title":"Proceedings of the 7th international workshop on formal methods for industrial critical systems (July 2002)","author":"Gallardo MM","year":"2002"},{"key":"p_17","volume-title":"Proceedings of the 11th international workshop on functional and (constraint) logic programming, electronic notes in theoretical computer science, vol 76","author":"Gallardo MM","year":"2002"},{"key":"p_18","first-page":"395","volume-title":"Proceedings of the 9th international static analysis symposium SAS '02","author":"Gallardo MM","year":"2002"},{"issue":"3","key":"p_19","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0743-1066(95)00038-0","article-title":"A generalized semantics and abstract interpretation for constraint logic programs","volume":"25","author":"Giacobazzi R","year":"1995","journal-title":"J Logic Programming"},{"key":"p_20","first-page":"72","volume-title":"Proceedings of the computer aided verification, LNCS-1254","author":"Gr S","year":"1997"},{"key":"p_21","volume-title":"Design and validation of computer protocols","author":"Hol GJ","year":"1991"},{"issue":"5","key":"p_22","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Hol GJ","year":"1997","journal-title":"IEEE Trans Softw Engin"},{"key":"p_23","volume-title":"The SPIN model checker. Primer and Reference Manual","author":"Hol GJ","year":"2003"},{"key":"p_24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384313","article-title":"Property preserving abstractions for the verification of concurrent systems","volume":"6","author":"Loiseaux C","year":"1995","journal-title":"Formal Methods Syst Des"},{"key":"p_25","volume-title":"The temporal logic of reactive and concurrent systems-Specification","author":"Ma Z","year":"1992"},{"key":"p_26","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1090\/dimacs\/032\/10","article-title":"Outline for an operational semantics of promela. In: the SPIN Verification Systems","volume":"32","author":"Na V","year":"1997","journal-title":"DIMACS Ser Discrete Math Theor Comput Sci"},{"key":"p_27","first-page":"3","volume-title":"Proceedings of the PSTV conference.","author":"Gerth R","year":"1995"},{"issue":"4","key":"p_28","doi-asserted-by":"crossref","first-page":"668","DOI":"10.1006\/jcss.2000.1744","article-title":"Verification by augmented abstraction: the automata-theoretic view","volume":"62","author":"Kesten Y","year":"2001","journal-title":"J Comput Syst Sci"},{"key":"p_29","first-page":"133","article-title":"A symbolic semantics for abstract model checking","volume":"39","author":"Lev F","year":"2001","journal-title":"Sci Comput Programming"},{"key":"p_31","first-page":"178","volume-title":"Proceedings of tools and algorithms for the construction and analysis of systems, LNCS-1579","author":"Ru V","year":"1999"},{"key":"p_32","first-page":"332","volume-title":"Proceedings of the Symposium on logic in computer science.","author":"Va MY","year":"1986"},{"key":"p_33","volume-title":"Proceedings the third SPIN workshop. http:\/\/netlib.belllabs.com\/netlib\/spin\/ws97\/papers.html","author":"Wei C","year":"1997"},{"key":"p_34","unstructured":"[Spin] On-the-fly LTL Model Checking with SPIN. http:\/\/spinroot.com\/spin\/whatispin.html"},{"key":"p_35","unstructured":"[\u03b1spin] \u03b1spin project. University of M\u00e1laga. http:\/\/www.lcc.uma.es\/gisum\/fmse\/tools"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0040-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0040-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0040-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:40:33Z","timestamp":1641483633000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0040-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["10.1007\/s00165-004-0040-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0040-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,8]]}}}