Close

1. Identity statement
Reference TypeJournal Article
Sitemtc-m21b.sid.inpe.br
Holder Codeisadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S
Identifier8JMKD3MGP5W34M/3HE6FCA
Repositorysid.inpe.br/mtc-m21b/2014/11.18.23.57.53   (restricted access)
Last Update2015:06.15.12.31.43 (UTC) administrator
Metadata Repositorysid.inpe.br/mtc-m21b/2014/11.18.23.57.54
Metadata Last Update2018:06.04.03.04.30 (UTC) administrator
DOI10.1007/978-3-319-09144-0_48
ISBN9783319091433
ISSN0302-9743
Labelscopus 2014-11 DosSantosErasSantVija:2014:FoVeTo
Citation KeySantosErasSantVija:2014:FoVeTo
TitleA formal verification tool for UML behavioral diagrams
Year2014
Access Date2024, June 15
Secondary TypePRE PI
Number of Files1
Size747 KiB
2. Context
Author1 Santos, Luciana Brasil Rebelo dos
2 Eras, Eduardo Rohde
3 Santiago Jr., Valdivino Alexandre de
4 Vijaykumar, Nandamudi Lankalapalli
Resume Identifier1
2
3
4 8JMKD3MGP5W/3C9JHTU
Group1 CAP-COMP-SPG-INPE-MCTI-GOV-BR
2 LAC-CTE-INPE-MCTI-GOV-BR
3 LAC-CTE-INPE-MCTI-GOV-BR
4 LAC-CTE-INPE-MCTI-GOV-BR
Affiliation1 Instituto Nacional de Pesquisas Espaciais (INPE)
2 Instituto Nacional de Pesquisas Espaciais (INPE)
3 Instituto Nacional de Pesquisas Espaciais (INPE)
4 Instituto Nacional de Pesquisas Espaciais (INPE)
e-Mail Addressmarcelo.pazos@inpe.br
JournalLecture Notes in Computer Science
Volume8579 LNCS
NumberPART 1
Pages696-711
Secondary MarkA1_ADMINISTRAÇÃO,_CIÊNCIAS_CONTÁBEIS_E_TURISMO A1_BIODIVERSIDADE A2_GEOGRAFIA B1_SAÚDE_COLETIVA B1_INTERDISCIPLINAR B1_CIÊNCIAS_SOCIAIS_APLICADAS_I B2_EDUCAÇÃO B2_ARQUITETURA_E_URBANISMO B3_MEDICINA_III B3_ENGENHARIAS_I B3_ENGENHARIAS_II B3_ODONTOLOGIA B3_GEOCIÊNCIAS B3_EDUCAÇÃO_FÍSICA B3_MEDICINA_I B3_MEDICINA_II B3_DIREITO B3_PSICOLOGIA B4_MATERIAIS B4_BIOTECNOLOGIA B5_MEDICINA_VETERINÁRIA B5_CIÊNCIAS_BIOLÓGICAS_I B5_CIÊNCIAS_BIOLÓGICAS_II B5_ENSINO C_ASTRONOMIA_/_FÍSICA C_CIÊNCIA_DA_COMPUTAÇÃO C_CIÊNCIAS_AGRÁRIAS_I C_ENGENHARIAS_III C_CIÊNCIAS_BIOLÓGICAS_III C_ENGENHARIAS_IV C_CIÊNCIAS_AMBIENTAIS C_MATEMÁTICA_/_PROBABILIDADE_E C_QUÍMICA
History (UTC)2018-06-04 03:04:30 :: administrator -> marcelo.pazos@inpe.br :: 2014
3. Content and structure
Is the master or a copy?is the master
Content Stagecompleted
Transferable1
Content TypeExternal Contribution
Version Typepublisher
KeywordsModel checking
Behavioral diagrams
Formal verification tools
Formal verifications
Modeling behavior
Object oriented software
Software model checking
State machine
Transition system
Unified Modeling Language
AbstractUnified Modeling Language (UML) is considered a standard for modeling object-oriented software. It supports several different diagrams that can be used to model behavior and structure of the software. With respect to formal verification, particularly Model Checking, the existing approaches are usually restricted to a single UML diagram. This paper presents a tool to convert UML behavioral diagrams (sequence, activity, and state machine) into Transition Systems to support software Model Checking. A peculiar feature of our tool is that it is developed as part of a larger effort to allow Model Checking of software built in accordance with UML, including several UML behavioral diagrams. We demonstrate the effectiveness of our approach by applying it to a classic case study and also to a real case study (embedded software) in the space domain. © 2014 Springer International Publishing.
AreaCOMP
Arrangement 1urlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > A formal verification...
Arrangement 2urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CAP > A formal verification...
doc Directory Contentaccess
source Directory Contentthere are no files
agreement Directory Contentthere are no files
4. Conditions of access and use
Languageen
User Groupadministrator
marcelo.pazos@inpe.br
Reader Groupadministrator
marcelo.pazos@inpe.br
Visibilityshown
Archiving Policydenypublisher denyfinaldraft12
Read Permissiondeny from all and allow from 150.163
Update Permissionnot transferred
5. Allied materials
Mirror Repositoryiconet.com.br/banon/2006/11.26.21.31
Next Higher Units8JMKD3MGPCW/3ESGTTP
8JMKD3MGPCW/3F2PHGS
Citing Item Listsid.inpe.br/bibdigital/2013/09.22.23.14 8
sid.inpe.br/mtc-m21/2012/07.13.14.56.50 2
sid.inpe.br/bibdigital/2013/10.12.22.16 1
DisseminationWEBSCI; PORTALCAPES; COMPENDEX; SCOPUS.
Host Collectionsid.inpe.br/mtc-m21b/2013/09.26.14.25.20
6. Notes
Empty Fieldsalternatejournal archivist callnumber copyholder copyright creatorhistory descriptionlevel electronicmailaddress format lineage mark month nextedition notes orcid parameterlist parentrepositories previousedition previouslowerunit progress project rightsholder schedulinginformation secondarydate secondarykey session shorttitle sponsor subject targetfile tertiarymark tertiarytype typeofwork url
7. Description control
e-Mail (login)marcelo.pazos@inpe.br
update 


Close