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 |