| 1. Identificação | |
| Tipo de Referência | Artigo em Revista Científica (Journal Article) |
| Código do Detentor | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S |
| Site | mtc-m21b.sid.inpe.br (namespace prefix: upn:3ET5SFU) |
| Identificador | 8JMKD3MGP5W34M/3HE6FCA |
| Repositório | sid.inpe.br/mtc-m21b/2014/11.18.23.57.53 (acesso restrito) |
| Última Atualização | 2015:06.15.12.31.43 (UTC) administrator |
| Repositório de Metadados | sid.inpe.br/mtc-m21b/2014/11.18.23.57.54 |
| Última Atualização dos Metadados | 2018:06.04.03.04.30 (UTC) administrator |
| DOI | 10.1007/978-3-319-09144-0_48 |
| ISBN | 9783319091433 |
| ISSN | 0302-9743 |
| Rótulo | scopus 2014-11 DosSantosErasSantVija:2014:FoVeTo |
| Chave de Citação | SantosErasSantVija:2014:FoVeTo |
| Título | A formal verification tool for UML behavioral diagrams  |
| Ano | 2014 |
| Data de Acesso | 20 set. 2026 |
| Tipo Secundário | PRE PI |
| Número de Arquivos | 1 |
| Tamanho | 747 KiB |
| 2. Contextualização | |
| Autor | 1 Santos, Luciana Brasil Rebelo dos 2 Eras, Eduardo Rohde 3 Santiago Jr., Valdivino Alexandre de 4 Vijaykumar, Nandamudi Lankalapalli |
| Identificador de Curriculo | 1 2 3 4 8JMKD3MGP5W/3C9JHTU |
| Grupo | 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 |
| Afiliação | 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) |
| Endereço de e-Mail | marcelo.pazos@inpe.br |
| Revista | Lecture Notes in Computer Science |
| Volume | 8579 LNCS |
| Número | PART 1 |
| Páginas | 696-711 |
| Nota Secundária | 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 |
| Acervo Hospedeiro | sid.inpe.br/mtc-m21b/2013/09.26.14.25.20 upn:3ET5SFU |
| Histórico (UTC) | 2018-06-04 03:04:30 :: administrator -> marcelo.pazos@inpe.br :: 2014 |
| 3. Conteúdo e estrutura | |
| É a matriz ou uma cópia? | é a matriz |
| Estágio do Conteúdo | concluido |
| Transferível | 1 |
| Tipo do Conteúdo | External Contribution |
| Tipo de Versão | publisher |
| Palavras-Chave | Model checking Behavioral diagrams Formal verification tools Formal verifications Modeling behavior Object oriented software Software model checking State machine Transition system Unified Modeling Language |
| Resumo | 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. |
| Área | COMP |
| Arranjo 1 | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > A formal verification... |
| Arranjo 2 | urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CAP > A formal verification... |
| Conteúdo da Pasta doc | acessar |
| Conteúdo da Pasta source | não têm arquivos |
| Conteúdo da Pasta agreement | não têm arquivos |
| 4. Condições de acesso e uso | |
| Idioma | en |
| Grupo de Usuários | administrator marcelo.pazos@inpe.br |
| Grupo de Leitores | administrator marcelo.pazos@inpe.br |
| Visibilidade | shown |
| Política de Arquivamento | denypublisher denyfinaldraft12 |
| Permissão de Leitura | deny from all and allow from 150.163 |
| Permissão de Atualização | não transferida |
| 5. Fontes relacionadas | |
| Repositório Espelho | iconet.com.br/banon/2006/11.26.21.31 |
| Unidades Imediatamente Superiores | 8JMKD3MGPCW/3ESGTTP 8JMKD3MGPCW/3F2PHGS |
| Lista de Itens Citando | sid.inpe.br/bibdigital/2013/09.22.23.14 - 91 sid.inpe.br/bibdigital/2013/10.12.22.16 - 73 sid.inpe.br/mtc-m21/2012/07.13.14.56.50 - 24 |
| Divulgação | WEBSCI; PORTALCAPES; COMPENDEX; SCOPUS. |
| 6. Notas | |
| Campos Vazios | 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. Controle da descrição | |
| e-Mail (login) | marcelo.pazos@inpe.br |
| atualizar | |