VeriAgent: An approach to integrating UML and formal verification tools

E. Mota; E. Clarke; A. Groce; W. Oliveira; M. Falcão; J. Kanda

doi:10.1016/j.entcs.2004.04.008

VeriAgent: An approach to integrating UML and formal verification tools

E. Mota, E. Clarke, A. Groce, W. Oliveira, M. Falcão, J. Kanda

Research output: Contribution to journal › Conference article › peer-review

12 Scopus citations

Abstract

The mathematical notations of Formal Verification Tools (FVTs) do not prevent us from wrongly defining the behavior of systems, any more than modern CASE tools do. With software rapidly growing in size and complexity, graphical specifications in languages like UML need to be formally verified, before the implementation phase, in order to guarantee the development of more reliable systems. While the enterprise of integrating CASE and FVTs has had reasonable success with the translation of simple diagrams to model checkers' notations, there has been few progress regarding the fundamental aspects an interface should have to fully integrate them. In this work we present an interface for joining both technologies as a reliable solution to bridging this gap.

Original language	English (US)
Pages (from-to)	111-129
Number of pages	19
Journal	Electronic Notes in Theoretical Computer Science
Volume	95
DOIs	https://doi.org/10.1016/j.entcs.2004.04.008
State	Published - May 17 2004
Externally published	Yes
Event	Proceedings of the Brazilian Workshop on Formal Methods - Campina Grande, Brazil Duration: Oct 12 2003 → Oct 14 2003

Keywords

Transformation
Verification Agent
Verification Tool

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/j.entcs.2004.04.008

Cite this

@article{33a76538d13c4739939206578a52d136,

title = "VeriAgent: An approach to integrating UML and formal verification tools",

abstract = "The mathematical notations of Formal Verification Tools (FVTs) do not prevent us from wrongly defining the behavior of systems, any more than modern CASE tools do. With software rapidly growing in size and complexity, graphical specifications in languages like UML need to be formally verified, before the implementation phase, in order to guarantee the development of more reliable systems. While the enterprise of integrating CASE and FVTs has had reasonable success with the translation of simple diagrams to model checkers' notations, there has been few progress regarding the fundamental aspects an interface should have to fully integrate them. In this work we present an interface for joining both technologies as a reliable solution to bridging this gap.",

keywords = "Transformation, Verification Agent, Verification Tool",

author = "E. Mota and E. Clarke and A. Groce and W. Oliveira and M. Falc{\~a}o and J. Kanda",

note = "Funding Information: 1 Work partially supported by CNPq/MCT-EsVIA Project, grant 550730/01-0. 2 mailto:{edjard,woliveira,marcia,jkanda}@ufam.edu.br 3 mailto:{emc,agroce}@cs.cmu.edu; Proceedings of the Brazilian Workshop on Formal Methods ; Conference date: 12-10-2003 Through 14-10-2003",

year = "2004",

month = may,

day = "17",

doi = "10.1016/j.entcs.2004.04.008",

language = "English (US)",

volume = "95",

pages = "111--129",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - VeriAgent

T2 - Proceedings of the Brazilian Workshop on Formal Methods

AU - Mota, E.

AU - Clarke, E.

AU - Groce, A.

AU - Oliveira, W.

AU - Falcão, M.

AU - Kanda, J.

N1 - Funding Information: 1 Work partially supported by CNPq/MCT-EsVIA Project, grant 550730/01-0. 2 mailto:{edjard,woliveira,marcia,jkanda}@ufam.edu.br 3 mailto:{emc,agroce}@cs.cmu.edu

PY - 2004/5/17

Y1 - 2004/5/17

N2 - The mathematical notations of Formal Verification Tools (FVTs) do not prevent us from wrongly defining the behavior of systems, any more than modern CASE tools do. With software rapidly growing in size and complexity, graphical specifications in languages like UML need to be formally verified, before the implementation phase, in order to guarantee the development of more reliable systems. While the enterprise of integrating CASE and FVTs has had reasonable success with the translation of simple diagrams to model checkers' notations, there has been few progress regarding the fundamental aspects an interface should have to fully integrate them. In this work we present an interface for joining both technologies as a reliable solution to bridging this gap.

AB - The mathematical notations of Formal Verification Tools (FVTs) do not prevent us from wrongly defining the behavior of systems, any more than modern CASE tools do. With software rapidly growing in size and complexity, graphical specifications in languages like UML need to be formally verified, before the implementation phase, in order to guarantee the development of more reliable systems. While the enterprise of integrating CASE and FVTs has had reasonable success with the translation of simple diagrams to model checkers' notations, there has been few progress regarding the fundamental aspects an interface should have to fully integrate them. In this work we present an interface for joining both technologies as a reliable solution to bridging this gap.

KW - Transformation

KW - Verification Agent

KW - Verification Tool

UR - http://www.scopus.com/inward/record.url?scp=18944396424&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944396424&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2004.04.008

DO - 10.1016/j.entcs.2004.04.008

M3 - Conference article

AN - SCOPUS:18944396424

SN - 1571-0661

VL - 95

SP - 111

EP - 129

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

Y2 - 12 October 2003 through 14 October 2003

ER -

VeriAgent: An approach to integrating UML and formal verification tools

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this