| 1. Identity statement | |
| Reference Type | Journal Article |
| Site | plutao.sid.inpe.br |
| Holder Code | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S |
| Identifier | 8JMKD3MGP3W/3KN36GH |
| Repository | sid.inpe.br/plutao/2015/12.04.14.22 (restricted access) |
| Last Update | 2020:09.14.15.03.54 (UTC) simone |
| Metadata Repository | sid.inpe.br/plutao/2015/12.04.14.22.42 |
| Metadata Last Update | 2020:09.14.15.03.54 (UTC) simone |
| ISSN | 0302-9743 |
| Label | lattes: 5039690360728170 3 ErasSantSantVija:2015:ApBaUM |
| Citation Key | ErasSantSantVija:2015:ApBaUM |
| Title | Towards a wide acceptance of formal methods to the design of safety critical software: an approach based on UML and model checking  |
| Year | 2015 |
| Access Date | 2024, Apr. 26 |
| Secondary Type | PRE PI |
| Number of Files | 1 |
| Size | 1299 KiB |
| 2. Context | |
| Author | 1 Eras, Eduardo Rohde 2 Santos, Luciana Brasil Rebelo dos 3 Santiago Júnior, Valdivino Alexandre de 4 Vijaykumar, Nandamudi Lankalapalli |
| Resume Identifier | 1 2 3 8JMKD3MGP5W/3C9JJB5 4 8JMKD3MGP5W/3C9JHTU |
| Group | 1 2 3 LAC-CTE-INPE-MCTI-GOV-BR 4 LAC-CTE-INPE-MCTI-GOV-BR |
| Affiliation | 1 2 3 Instituto Nacional de Pesquisas Espaciais (INPE) 4 Instituto Nacional de Pesquisas Espaciais (INPE) |
| Author e-Mail Address | 1 2 3 valdivino.santiago@inpe.br 4 vijay.nl@inpe.br |
| Journal | Lecture Notes in Computer Science |
| Volume | 9158 |
| Pages | 612-627 |
| Secondary Mark | A1_BIODIVERSIDADE A1_ADMINISTRAÇÃO,_CIÊNCIAS_CONTÁBEIS_E_TURISMO A2_GEOGRAFIA B1_SAÚDE_COLETIVA B1_INTERDISCIPLINAR B1_CIÊNCIAS_SOCIAIS_APLICADAS_I B2_EDUCAÇÃO B2_ARQUITETURA_E_URBANISMO B3_PSICOLOGIA B3_ODONTOLOGIA B3_MEDICINA_III B3_MEDICINA_II B3_MEDICINA_I B3_GEOCIÊNCIAS B3_ENGENHARIAS_II B3_ENGENHARIAS_I B3_EDUCAÇÃO_FÍSICA B3_DIREITO B4_MATERIAIS B4_BIOTECNOLOGIA B5_MEDICINA_VETERINÁRIA B5_ENSINO B5_CIÊNCIAS_BIOLÓGICAS_II B5_CIÊNCIAS_BIOLÓGICAS_I C_QUÍMICA C_MATEMÁTICA_/_PROBABILIDADE_E_ESTATÍSTICA C_ENGENHARIAS_IV C_ENGENHARIAS_III C_CIÊNCIAS_BIOLÓGICAS_III C_CIÊNCIAS_AMBIENTAIS C_CIÊNCIAS_AGRÁRIAS_I C_CIÊNCIA_DA_COMPUTAÇÃO C_ASTRONOMIA_/_FÍSICA |
| History (UTC) | 2015-12-04 14:22:42 :: lattes -> administrator :: 2018-06-04 23:25:57 :: administrator -> simone :: 2015 |
| 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 UML Formal Methods Formal Verification |
| Abstract | The Unified Modeling Language (UML) is widely used to model systems for object oriented and/or embedded software development, specially by means of its several behavioral diagrams which can provide different points of view of the same software scenario. Model Checking is a formal verification method which has been receiving much attention from the academic community. However, in general, practitioners still avoid using Model Checking in their projects due to several reasons. Based on these facts, we present in this paper a significant improvement of a tool that we have developed which aims to translate several UML behavioral diagrams (sequence, activity, and state machine) into Transition Systems to support software Model Checking. With all the changes, we have applied our tool to a real space software product which is under development for a stratospheric balloon project to show how feasible is our approach in practice. |
| Area | COMP |
| Arrangement | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > LABAC > Towards a wide... |
| 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 |
| Target File | eras_towards.pdf |
| User Group | lattes simone |
| Reader Group | administrator simone |
| 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 | urlib.net/www/2011/03.29.20.55 |
| Next Higher Units | 8JMKD3MGPCW/3ESGTTP |
| Citing Item List | sid.inpe.br/bibdigital/2013/09.22.23.14 1 sid.inpe.br/mtc-m21/2012/07.13.15.01.24 1 |
| URL (untrusted data) | http://link.springer.com/chapter/10.1007%2F978-3-319-21410-8_47 |
| Dissemination | WEBSCI; PORTALCAPES; COMPENDEX; SCOPUS. |
| Host Collection | dpi.inpe.br/plutao@80/2008/08.19.15.01 |
| 6. Notes | |
| Notes | Setores de Atividade: Pesquisa e desenvolvimento científico. |
| Empty Fields | alternatejournal archivist callnumber copyholder copyright creatorhistory descriptionlevel doi e-mailaddress format isbn lineage mark month nextedition number orcid parameterlist parentrepositories previousedition previouslowerunit progress project rightsholder schedulinginformation secondarydate secondarykey session shorttitle sponsor subject tertiarymark tertiarytype typeofwork |
| 7. Description control | |
| e-Mail (login) | simone |
| update | |