| 1. Identity statement | |
| Reference Type | Journal Article |
| Site | mtc-m21b.sid.inpe.br |
| Holder Code | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S |
| Identifier | 8JMKD3MGP5W34M/3HE6FCA |
| Repository | sid.inpe.br/mtc-m21b/2014/11.18.23.57.53 (restricted access) |
| Last Update | 2015:06.15.12.31.43 (UTC) administrator |
| Metadata Repository | sid.inpe.br/mtc-m21b/2014/11.18.23.57.54 |
| Metadata Last Update | 2018:06.04.03.04.30 (UTC) administrator |
| DOI | 10.1007/978-3-319-09144-0_48 |
| ISBN | 9783319091433 |
| ISSN | 0302-9743 |
| Label | scopus 2014-11 DosSantosErasSantVija:2014:FoVeTo |
| Citation Key | SantosErasSantVija:2014:FoVeTo |
| Title | A formal verification tool for UML behavioral diagrams  |
| Year | 2014 |
| Access Date | 2024, July 27 |
| Secondary Type | PRE PI |
| Number of Files | 1 |
| Size | 747 KiB |
| 2. Context | |
| Author | 1 Santos, Luciana Brasil Rebelo dos 2 Eras, Eduardo Rohde 3 Santiago Jr., Valdivino Alexandre de 4 Vijaykumar, Nandamudi Lankalapalli |
| Resume Identifier | 1 2 3 4 8JMKD3MGP5W/3C9JHTU |
| Group | 1 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 |
| Affiliation | 1 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 Address | marcelo.pazos@inpe.br |
| Journal | Lecture Notes in Computer Science |
| Volume | 8579 LNCS |
| Number | PART 1 |
| Pages | 696-711 |
| Secondary Mark | A1_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 Stage | completed |
| Transferable | 1 |
| Content Type | External Contribution |
| Version Type | publisher |
| Keywords | Model checking Behavioral diagrams Formal verification tools Formal verifications Modeling behavior Object oriented software Software model checking State machine Transition system Unified Modeling Language |
| Abstract | Unified 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. |
| Area | COMP |
| Arrangement 1 | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > A formal verification... |
| Arrangement 2 | urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CAP > A formal verification... |
| doc Directory Content | access |
| source Directory Content | there are no files |
| agreement Directory Content | there are no files |
| 4. Conditions of access and use | |
| Language | en |
| User Group | administrator marcelo.pazos@inpe.br |
| Reader Group | administrator marcelo.pazos@inpe.br |
| Visibility | shown |
| Archiving Policy | denypublisher denyfinaldraft12 |
| Read Permission | deny from all and allow from 150.163 |
| Update Permission | not transferred |
| 5. Allied materials | |
| Mirror Repository | iconet.com.br/banon/2006/11.26.21.31 |
| Next Higher Units | 8JMKD3MGPCW/3ESGTTP 8JMKD3MGPCW/3F2PHGS |
| Citing Item List | sid.inpe.br/bibdigital/2013/09.22.23.14 12 sid.inpe.br/bibdigital/2013/10.12.22.16 5 sid.inpe.br/mtc-m21/2012/07.13.14.56.50 3 |
| Dissemination | WEBSCI; PORTALCAPES; COMPENDEX; SCOPUS. |
| Host Collection | sid.inpe.br/mtc-m21b/2013/09.26.14.25.20 |
| 6. Notes | |
| Empty Fields | alternatejournal 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 | |