Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/17801| Título: | An integrated formal methods tool-chain and its application to verifying a file system model |
| Autor(es): | Ferreira, Miguel A. Oliveira, José Nuno Fonseca |
| Palavras-chave: | Grand challenges in computing Formal methods |
| Data: | 2009 |
| Editora: | Springer Verlag |
| Revista: | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Resumo(s): | Tool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel (R) Flash File System Core. We combine high-level manual specification and proofs with current state of the art mechanical verification tools into a tool-chain which involves Alloy, VDM++ and HOL. The use of (pointfree) relation modelling provides the glue which binds these tools together. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/17801 |
| ISBN: | 978-3-642-10451-0 |
| DOI: | 10.1007/978-3-642-10452-7_11 |
| ISSN: | 0302-9743 |
| Versão da editora: | http://www.springerlink.com/content/uk242017ptr06736/ |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
| Ficheiro | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| sbmf09 copy.pdf | 220,87 kB | Adobe PDF | Ver/Abrir |
