Mostrar el registro sencillo del ítem
Automatic generation of assumptions for modular verification of software specifications
dc.contributor.author | Riva Álvarez, Claudio A. de la | |
dc.contributor.author | Tuya González, Pablo Javier | |
dc.date.accessioned | 2015-02-11T12:39:10Z | |
dc.date.available | 2015-02-11T12:39:10Z | |
dc.date.issued | 2006 | |
dc.identifier.citation | Journal of Systems and Software, 79(9), p. 1324-1340 (2006); doi:10.1016/j.jss.2005.11.570 | |
dc.identifier.issn | 0164-1212 | |
dc.identifier.uri | http://hdl.handle.net/10651/29644 | |
dc.description.abstract | Model checking is a powerful automated technique mainly used for the verification of properties of reactive systems. In practice, model checkers are limited due to the state explosion problem. Modular verification based on the assume-guarantee paradigm mitigates this problem using a “divide and conquer” technique. Unfortunately, this approach is not automated, for the reason that the user must specify the environment model. In this paper, a novel technique is presented for automatically generating component assumptions based on the behaviour of the environment (the remainder of components of the systems). In a first phase, the environment of the component is computed using state space exploration techniques, and then the assumptions are generated as association rules of the component environment interface. This approach presents a number of advantages. Firstly, user assistance to specify assumptions is not necessary and assumption discharge is avoided. Secondly, the component assumptions are more restrictive and real, and therefore reduce the resources needed by the model checker. The technique is applied to the specification of a steam boiler system | |
dc.format.extent | p. 1324-1340 | spa |
dc.language.iso | eng | spa |
dc.publisher | Elsevier | |
dc.relation.ispartof | Journal of Systems and Software, 79(9) | spa |
dc.rights | © Elsevier | |
dc.rights | CC Reconocimiento - No comercial - Sin obras derivadas 4.0 Internacional | |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | |
dc.subject | Assume-guarantee reasoning | |
dc.subject | Model checking | |
dc.subject | Modular verification | |
dc.subject | Component verification | |
dc.title | Automatic generation of assumptions for modular verification of software specifications | spa |
dc.type | journal article | |
dc.identifier.doi | 10.1016/j.jss.2005.11.570 | |
dc.relation.publisherversion | http://dx.doi.org/10.1016/j.jss.2005.11.570 | |
dc.rights.accessRights | open access |
Ficheros en el ítem
Este ítem aparece en la(s) siguiente(s) colección(ones)
-
Artículos [34664]
-
Informática [759]