Specification of Real-Time Systems with Graph Grammars
Resumo
Este artigo apresenta uma abordagem formal para a especificação e análise de sistemas de tempo real. Gramáticas de Grafos Baseadas em Objetos são extendidas incluindo primitivas para modelar explicitamente restrições de tempo.. A semântica é definida em termos de autômatos temporais, provendo um método para verificação automática de propriedades.
Referências
Alur, R. and Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126(2):183–235.
Baeten, J. and Middelburg, C. (2000). Process algebra with timing: Real time and discrete time. In Handbook of Process Algebra, chapter 4. Elsevier.
Behrmann, G., David, A., and Larsen, K. G. (2004). Tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems, volume 3185 of LNCS, pages 200–236. Springer.
Bengtsson, J. and Yi, W. (2004). Timed automata: Semantics, algorithms and tools. In Lecture Notes on Concurrency and Petri Nets, volume 3098 of LNCS, pages 87–124. Springer.
Berthomieu, B. and Diaz, M. (1991). Modeling and verification of time dependent systems using time petri nets. IEEE Trans. Softw. Eng., 17(3):259–273.
Bowman, H. and Derrick, J. (1997). Extending lotos with time: A true concurrency perspective. In AMAST Workshop on Real-Time Systems, Concurrent and Distributed Software, volume 1231 of LNCS, pages 382–399. Springer.
Clarke, E. M. and Wing, J. M. (1996). Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626–643.
Corradini, A., Montanari, U., and Rossi, F. (1996). Graph processes. Fundamenta Informaticae, 26(3/4):241–265.
Diethers, K. and Huhn, M. (2004). Vooduu: Verification of object-oriented designs using uppaal. In Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of LNCS, pages 139–143. Springer.
Dotti, F. L., Foss, L., Ribeiro, L., and Santos, O. M. (2003). Verification of distributed object-based systems. In 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 261–275. Springer.
Dotti, F. L. and Ribeiro, L. (2000). Specification of mobile code systems using graph grammars. In Formal Methods for Open Object-Based Distributed Systems, pages 45–64. Kluwer.
Duarte, L. M., Dotti, F. L., Copstein, B., and Ribeiro, L. (2002). Simulation of mobile applications. In Proc. of Communication Networks and Distributed Systems Modeling and Simulation Conference, volume 1, pages 1–15.
Ehrig, H. and Mahr, B. (1985). Fundamentals of algebraic specification: Equations and initial algebra semantics. In EATCS Monographs on Theoretical Computer Science, volume 6. Springer.
Ferreira, A. P. L. (2005). Object-Oriented Graph Grammars. PhD thesis, Universidade Federal do Rio Grande do Sul.
Graf, S., Ober, I., and Ober, I. (2003). Timed annotations with UML. In Workshop on Specification and Validation of UML models for Real Time and Embedded Systems.
Knapp, A., Merz, S., and Rauh, C. (2002). Model checking timed uml state machines and collaborations. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 395–416. Springer.
Konrad, S., Campbell, L. A., and Cheng, B. H. C. (2004). Automated analysis of timing information in uml diagrams. In Proceedings of the 19th IEEE international conference on Automated software engineering, pages 350–353. IEEE Computer Society.
Lavazza, L., Quaroni, G., and Venturelli, M. (2001). Combining uml and formal notations for modelling real-time systems. SIGSOFT Softw. Eng. Notes, 26(5):196–206.
Lee, I., Bremond-Gregoire, P., and Gerber, R. (1994). A process algebraic approach to the specification and analysis of resource-bound real-time systems. Proc. of the IEEE, 82(1):158–171.
Ober, I., Graf, S., and Ober, I. (2004). Validation of uml models via a mapping to communicating extended timed automata. In SPIN, volume 2989 of LNCS, pages 127–145. Springer.
Ribeiro, L., Dotti, F., and Bardohl, R. (2005). A formal framework for the development of concurrent object-based systems. In Formal Methods in Software and Systems Modeling, volume 3393 of LNCS, pages 385–401. Springer.
Ribeiro, L., Dotti, F. L., Santos, O., and Pasini, F. (2006). Verifying object-based graph grammars: An assume-guarantee approach. Accepted for publication in Software and Systems Modeling.
Stankovic, J. A. (1988). A serious problem for next-generation systems. IEEE Computer, 21(10):10–19.
Stankovic, J. A. et al. (1996). Strategic directions in real-time and embedded systems. ACM Computing Surveys, 28(4):751–763.
Walter, B. (1983). Timed petri-nets for modelling and alalyzing protocols with real-time characteristics. In Protocol Specification, Testing, and Verification, pages 149–159. North-Holand.
Baeten, J. and Middelburg, C. (2000). Process algebra with timing: Real time and discrete time. In Handbook of Process Algebra, chapter 4. Elsevier.
Behrmann, G., David, A., and Larsen, K. G. (2004). Tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems, volume 3185 of LNCS, pages 200–236. Springer.
Bengtsson, J. and Yi, W. (2004). Timed automata: Semantics, algorithms and tools. In Lecture Notes on Concurrency and Petri Nets, volume 3098 of LNCS, pages 87–124. Springer.
Berthomieu, B. and Diaz, M. (1991). Modeling and verification of time dependent systems using time petri nets. IEEE Trans. Softw. Eng., 17(3):259–273.
Bowman, H. and Derrick, J. (1997). Extending lotos with time: A true concurrency perspective. In AMAST Workshop on Real-Time Systems, Concurrent and Distributed Software, volume 1231 of LNCS, pages 382–399. Springer.
Clarke, E. M. and Wing, J. M. (1996). Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626–643.
Corradini, A., Montanari, U., and Rossi, F. (1996). Graph processes. Fundamenta Informaticae, 26(3/4):241–265.
Diethers, K. and Huhn, M. (2004). Vooduu: Verification of object-oriented designs using uppaal. In Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of LNCS, pages 139–143. Springer.
Dotti, F. L., Foss, L., Ribeiro, L., and Santos, O. M. (2003). Verification of distributed object-based systems. In 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 261–275. Springer.
Dotti, F. L. and Ribeiro, L. (2000). Specification of mobile code systems using graph grammars. In Formal Methods for Open Object-Based Distributed Systems, pages 45–64. Kluwer.
Duarte, L. M., Dotti, F. L., Copstein, B., and Ribeiro, L. (2002). Simulation of mobile applications. In Proc. of Communication Networks and Distributed Systems Modeling and Simulation Conference, volume 1, pages 1–15.
Ehrig, H. and Mahr, B. (1985). Fundamentals of algebraic specification: Equations and initial algebra semantics. In EATCS Monographs on Theoretical Computer Science, volume 6. Springer.
Ferreira, A. P. L. (2005). Object-Oriented Graph Grammars. PhD thesis, Universidade Federal do Rio Grande do Sul.
Graf, S., Ober, I., and Ober, I. (2003). Timed annotations with UML. In Workshop on Specification and Validation of UML models for Real Time and Embedded Systems.
Knapp, A., Merz, S., and Rauh, C. (2002). Model checking timed uml state machines and collaborations. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 395–416. Springer.
Konrad, S., Campbell, L. A., and Cheng, B. H. C. (2004). Automated analysis of timing information in uml diagrams. In Proceedings of the 19th IEEE international conference on Automated software engineering, pages 350–353. IEEE Computer Society.
Lavazza, L., Quaroni, G., and Venturelli, M. (2001). Combining uml and formal notations for modelling real-time systems. SIGSOFT Softw. Eng. Notes, 26(5):196–206.
Lee, I., Bremond-Gregoire, P., and Gerber, R. (1994). A process algebraic approach to the specification and analysis of resource-bound real-time systems. Proc. of the IEEE, 82(1):158–171.
Ober, I., Graf, S., and Ober, I. (2004). Validation of uml models via a mapping to communicating extended timed automata. In SPIN, volume 2989 of LNCS, pages 127–145. Springer.
Ribeiro, L., Dotti, F., and Bardohl, R. (2005). A formal framework for the development of concurrent object-based systems. In Formal Methods in Software and Systems Modeling, volume 3393 of LNCS, pages 385–401. Springer.
Ribeiro, L., Dotti, F. L., Santos, O., and Pasini, F. (2006). Verifying object-based graph grammars: An assume-guarantee approach. Accepted for publication in Software and Systems Modeling.
Stankovic, J. A. (1988). A serious problem for next-generation systems. IEEE Computer, 21(10):10–19.
Stankovic, J. A. et al. (1996). Strategic directions in real-time and embedded systems. ACM Computing Surveys, 28(4):751–763.
Walter, B. (1983). Timed petri-nets for modelling and alalyzing protocols with real-time characteristics. In Protocol Specification, Testing, and Verification, pages 149–159. North-Holand.
Publicado
16/10/2006
Como Citar
MICHELON, Leonardo; COSTA, Simone André da; RIBEIRO, Leila.
Specification of Real-Time Systems with Graph Grammars. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 20. , 2006, Florianópolis.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2006
.
p. 97-112.
DOI: https://doi.org/10.5753/sbes.2006.21207.
