Verificação formal de protocolos TDMA quanto a características de tempo real e tolerância a falhas
Resumo
Este trabalho apresenta uma metodologia para representar protocolos TDMA e possíveis falhas que possam ocorrer em sistemas de tempo real tolerantes a falhas utilizando métodos automáticos de verificação. Isto permite garantir diversas propriedades qualitativas e resultados quantitativos como o limite superior de tempo para atingir tais propriedades. Como estudo de caso, apresenta a representação do protocolo TTP/C, determinando o limite de tempo máximo para se atingir a auto-estabilização das visões que cada nodo possui do sistema (Group-membership), possibilitando garantir o tempo máximo de recuperação do sistema, em um cenário de falhas.
Referências
CLARKE, E. EMERSON, E. Design and synthesis of syncronization skeletons using branching time temporal logic. Workshop on logics of programs, v.131, of Lectures Notes in Computer Science, p.52-71. 1981.
BRYANT, R. E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, v.C-35, n.8, 1986.
JOHNSON, B. Design and Analysis of Fault-Tolerant Digital Systems. 1.ed. Addison-Wesley series in electrical and computer engineering, 1989. 584p.
CRISTIAN, F. Reaching Agreement on Processor Group Membership in Synchronous Distributed System. Distributed Computing, v.4, p.175-187, 1991.
KOPETZ, H. GRUNSTEIDL, G., TTP - A protocol for fault-tolerant real time systems, IEEE Computer, v.27#1, p.14-23. Jan 1994.
JALOTE, P., Fault tolerance in distributed Systems. Prentice-Hall, 1994. 432p.
CAMPOS, S. et al. Verifying the performance of the PCI local bus using symbolic techniques. International Conference on Computer Design, 1995.
BIRMAN, K. Buildin secure and reliable network applications. Manning Publications Co, 1996.
CAMPOS, S. CLARK, E. MINEA, M. The Verus tool: a quantitative approach to the formal verification of real-time systems. Conference on Computer Aided Verification, 1997.
PASCOE, J. LOADER, R. SUNDERAM, V. Working towards the agreement problem protocol verification environment. Communications Process Architectures, 2001.
TTP/C Specification 1.0, Disponível em: <http://www.tttech.com>, Acesso em 26 mar. 2003.
ISO.Road Vehicles Controller Area Network (CAN) Part 4: TimeTriggered Comunication. Standard ISO/CD 11898-4, International Organization for Standardization, 2001
BRYANT, R. E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, v.C-35, n.8, 1986.
JOHNSON, B. Design and Analysis of Fault-Tolerant Digital Systems. 1.ed. Addison-Wesley series in electrical and computer engineering, 1989. 584p.
CRISTIAN, F. Reaching Agreement on Processor Group Membership in Synchronous Distributed System. Distributed Computing, v.4, p.175-187, 1991.
KOPETZ, H. GRUNSTEIDL, G., TTP - A protocol for fault-tolerant real time systems, IEEE Computer, v.27#1, p.14-23. Jan 1994.
JALOTE, P., Fault tolerance in distributed Systems. Prentice-Hall, 1994. 432p.
CAMPOS, S. et al. Verifying the performance of the PCI local bus using symbolic techniques. International Conference on Computer Design, 1995.
BIRMAN, K. Buildin secure and reliable network applications. Manning Publications Co, 1996.
CAMPOS, S. CLARK, E. MINEA, M. The Verus tool: a quantitative approach to the formal verification of real-time systems. Conference on Computer Aided Verification, 1997.
PASCOE, J. LOADER, R. SUNDERAM, V. Working towards the agreement problem protocol verification environment. Communications Process Architectures, 2001.
TTP/C Specification 1.0, Disponível em: <http://www.tttech.com>, Acesso em 26 mar. 2003.
ISO.Road Vehicles Controller Area Network (CAN) Part 4: TimeTriggered Comunication. Standard ISO/CD 11898-4, International Organization for Standardization, 2001
Publicado
19/05/2003
Como Citar
BECKLER, Alberto Rubens; CAMPOS, Sérgio Vale Aguiar.
Verificação formal de protocolos TDMA quanto a características de tempo real e tolerância a falhas. In: WORKSHOP DE TESTES E TOLERÂNCIA A FALHAS (WTF), 4. , 2003, Natal/RN.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2003
.
p. 53-60.
ISSN 2595-2684.
DOI: https://doi.org/10.5753/wtf.2003.23390.
