Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/18102| Título: | Model of mechanism behavior for verification of PLC programs |
| Autor(es): | Machado, José Mendes Denis, Bruno Lesage, Jean-Jacques Faure, Jean-Marc Silva, Jaime F. da |
| Palavras-chave: | Discrete event systems Plant model Formal verification Model-checking |
| Data: | 2004 |
| Editora: | Associação Brasileira de Engenharia e Ciências Mecânicas (ABCM) |
| Citação: | ABCM Symposium Series in Mechatronics |
| Resumo(s): | More extensive work on formal methods is now available for checking PLC (Programmable Logic Controller) programs. To verify a PLC program, it is necessary to consider a set of properties to prove and one of the most interesting problems that the designers must deal is to deduce a set of properties that traduces all the safety requirements of the system behavior. In this paper, we explore the contribution of such a plant model within the context of deduction, in a systematized way, of a set of properties to prove, verifying the PLC program. Our study is primarily experimental in nature and based on a case study. A set of properties to be checked based on detailed plant model is proposed. We then analyze how a Symbolic Model-Checking tool (the NuSMV has been selected) ensures verification of these properties either with or without the considered plant model. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/18102 |
| ISBN: | 85-857699-20-3 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: | DEM - Artigos em revistas de circulação internacional com arbitragem científica |
Ficheiros deste registo:
| Ficheiro | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| SSM_IV_06.pdf | 272,38 kB | Adobe PDF | Ver/Abrir |
