Early Verification of Software Behavior in a Time Interval Framework

• Paulo Sérgio Muniz Silva USP

DOI: https://doi.org/10.5753/sbes.2003.23864

Resumo

Verification of software behavior in early moments of the development process is not an easy task. Typically, software engineers draw diagrams to reason about the software functional behavior, for example, drawing Message Sequence Charts (MSCs). Not always does the intended behavior described by MSCs correspond to their actual behavior. To help the verification of the actual behavior of MSCs, this paper describes an interpretation of (basic) MSCs in a temporal framework that formally represents the qualitative, and possibly imprecise, temporal information conveyed in MSCs. The framework is an algebra of binary relations on time intervals, and provides rules of reasoning about the temporal information. The interpretation provides a polynomialtime solution to the verification problem and lays the foundations of a model checking tool.

Palavras-chave: formal verification and validation, requirements model checking, temporal reasoning

Referências

Allen, J. F. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983.

Allen, J. F. Towards a general theory of action and time. Artificial Intelligence, 23(2), 123-154.

Allen, J. F. Temporal reasoning and planning. In Allen, J. F. and Kautz, H. A. and Pelavin, R. N. and Teneberg, J. D., editors, Reasoning about Plans, pages 1-67. Morgan Kaufmann, 1991.

Alur, R., Etessami, K. and Yannakakis, M. Inference of message sequence charts. In 22nd International Conference on Software Engineering, pages 304-313, 2000.

Alur, R., Holzmann, G. J. and Peled, D. An analyzer for message sequence charts. In Margaria, T. and Steffen, B., editors, Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in LNCS, pages 35-48. Springer-Verlag, 1996.

Alur, R. and Yannakakis, M. Model checking of message sequence charts. In CONCUR '99: Concurrency Theory, Tenth International Conference, number 1664 in LNCS, pages 114-129. Springer-Verlag, 1999.

Ben-Abdallah, H. and Leue, S. Expressing and analyzing timing constraints in message sequence chart specifications. Technical Report 97-04, Department of Electrical and Computer Engineering, University of Waterloo, 1997.

Drakengren, T. and Jonsson, P. Eight maximal tractable subclasses of Allen's algebra with metric time. Journal of Artificial Intelligence Research, 7:25-45, 1997.

Holzmann, G. Early fault detection tools. In Margaria, T. and Steffen, B., editors, Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in LNCS, pages 1-13. Springer-Verlag, 1996.

ITU-T. Recommendation Z.120 Annex B: Algebraic semantics of message sequence charts. ITU-TS, Geneva, Swiss, April 1995.

ITU-T. Recommendation Z.120. Message sequence charts (MSC'96). ITU-TS, Geneva, Swiss, April 1996.

Jacobson, I. et al. Object-Oriented Software Engineering a Use Case Driven Approach. Addison-Wesley Publishing Co., London, 1992.

Ladkin, P. B. and Leue, S. Interpreting message flow graphs. Formal Aspects of Computing, 7(5):473-509, 1995.

Ladkin, P. B. and Maddux, R. On binary constraint problems. Journal of the ACM, 41(3):435-469, 1994.

Mackworth, A. K. Consistency in networks of relations. Artificial Intelligence, 8:99-118, 1997.

Mauw, S. and Reniers, M. A. An algebraic semantics of basic message sequence charts. The Computer Journal, 37(4):269-277, 1994.

Mauw, S. and Reniers, M. A. Operational semantics for MSC'96. Computer Networks and ISDN Systems, 31(17):1785-1799, 1999.

Montanari, U. Networks of constraints: fundamental properties and applications to picture processing. Information Science, 7:95-132, 1994.

Muniz Silva, P. S. Extended message sequence charts with time-interval semantics. In Proceedings of the Fifth International Workshop on Temporal Representation and Reasoning, pages 37-44, Sanibel Island, FL, USA, 1998.

Muscholl, A. and Peled, D. Message sequence graphs and decision problems in Mazurkiewicz traces. In Proceedings of MFCS, number 1672 in LNCS, pages 81-91. Springer-Verlag, 1999.

Muscholl, A. and Peled, D. and Su, Z. Deciding properties for message sequence charts. In Proceedings of FoSSaCS'98, number 1378 in LNCS, pages 226-242. Springer-Verlag, 1998.

Nebel, B. and Bürckert, H-J. Reasoning about temporal relations: a maximal tractable subclass of Allen's interval algebra. Journal of the ACM, 42(1):43-66, 1995.

Nebel, B. and Bürckert, H-J. Software for machine assisted analysis of Allen's interval algebra. Available from [link], 1995.

OMG. OMG Unified Modeling Language Specification version 1.4. Object Management Group, Inc., USA, September 2001.

Turski, W. M. and Maibaum, T. S. The specification of computer programs. Addison-Wesley Publishing Co., London, 1987.

Uchitel, S. Incremental Elaboration of Scenario-Based Specifications and Behaviour Models Using Implied Scenarios. PhD thesis, Imperial College of Science, Technology and Medicine. University of London, Department of Computing, 2003.

van Beek, P. G. Reasoning about qualitative temporal information. Artificial Intelligence, 58:297-326, 1992.

van Beek, P. G. and Cohen, R. Exact and approximate reasoning about temporal relations. Computational Intelligence, 6(3):132-144, 1990.

Vilain, M. B. and Kautz, H. A. Constraint propagation algorithms for temporal reasoning. In Proceedings of the Fifth National Conference of the American Association for Artificial Intelligence, pages 366-382, Philadelphia, PA, USA, 1986.

Weida, R. and Litman, D. Terminological reasoning with constraint networks and an application to plan recognition. In Nebel, B., Swartout, W. and Rich, C., editors, Principles of knowledge representation and reasoning: Proceedings of the Third International Conference, pages 282-293, Cambridge, MA, USA, 1992.