×

Stepwise refinement of sequence diagrams with soft real-time constraints. (English) Zbl 1320.68040

Summary: UML sequence diagrams and similar notations are much used to specify and analyze computer systems and their requirements. Probabilities are often essential, in particular for capturing soft real-time constraints. It is also important to be able to specify systems at different levels of abstraction. Refinement is a means to relate abstract specifications to more concrete specifications in such a way that constraints and analysis results are preserved through the transition. In order to allow soft real-time constraints to be included as an integral part of sequence diagram specifications, this paper presents an approach to extend UML 2.x sequence diagrams to capture probabilistic choice in general and soft real-time constraints in particular. The approach is supported by formal semantics and pragmatic refinement relations with mathematical properties that allow stepwise and modular development of specifications. An example focusing on communication is provided to demonstrate the language and refinement relations.

MSC:

68M12 Network protocols
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

MARTE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Dobing, B.; Parsons, J., How UML is used, Commun. ACM, 49, 5, 109-113 (2006)
[3] Mauw, S.; Reniers, M. A.; Willemse, T. A.C., Message sequence charts in the software engineering process, (Handbook of Software Engineering and Knowledge Engineering (2001), World Scientific), 437-463
[4] Haugen, Ø.; Husa, K. E.; Runde, R. K.; Stølen, K., STAIRS towards formal design with sequence diagrams, J. Softw. Syst. Model., 22, 4, 349-458 (2005)
[5] Runde, R. K.; Haugen, Ø.; Stølen, K., Refining UML interactions with underspecification and nondeterminism, Nord. J. Comput., 12, 2, 157-188 (2005) · Zbl 1087.68023
[6] Haugen, Ø.; Husa, K. E.; Runde, R. K.; Stølen, K., Why timed sequence diagrams require three-event semantics, (Proc. Scenarios: Models, Transformations and Tools. Proc. Scenarios: Models, Transformations and Tools, LNCS, vol. 3466 (2005), Springer), 1-25
[8] Refsdal, A.; Jacobsson, S., Adding soft real-time requirements in a step-wise development process, Telektronikk, 105, 1, 69-80 (2009)
[9] Jones, C. B., Systematic Software Development Using VDM (1986), Prentice-Hall · Zbl 0584.68008
[11] Refsdal, A.; Runde, R. K.; Stølen, K., Underspecification, inherent nondeterminism and probability in sequence diagrams, (Proc. 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems. Proc. 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS. Proc. 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems. Proc. 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS, LNCS, vol. 4037 (2006), Springer), 138-155 · Zbl 1461.68117
[12] Runde, R. K.; Refsdal, A.; Stølen, K., Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism, Form. Asp. Comput., 25, 159-187 (2013) · Zbl 1259.68133
[13] Back, R.-J.; von Wright, J., Refinement Calculus - a Systematic Introduction, Undergraduate Texts in Computer Science (1999), Springer
[14] Refsdal, A.; Husa, K. E.; Stølen, K., Specification and refinement of soft real-time requirements using sequence diagrams (2007), Department of Informatics, University of Oslo, Technical Report 323
[15] Olderog, E.-R.; Dierks, H., Real-Time Systems - Formal Specification and Automatic Verification (2008), Cambridge University Press · Zbl 1161.68030
[16] Lund, M. S.; Stølen, K., A fully operational semantics for UML 2.0 sequence diagrams with potential and mandatory choice, (Proc. 14th International Symposium on Formal Methods. Proc. 14th International Symposium on Formal Methods, LNCS, vol. 4085 (2006), Springer), 380-395
[17] Lund, M. S., Operational analysis of sequence diagram specifications (2008), University of Oslo, PhD thesis
[18] Micskei, Z.; Waeselynck, H., The many meanings of UML 2 sequence diagrams: a survey, Softw. Syst. Model., 10, 4, 489-514 (2011)
[19] Cengarle, M. V.; Knapp, A., UML 2.0 interactions: semantics and refinement, (Proc. 3rd International Workshop on Critical Systems Development with UML. Proc. 3rd International Workshop on Critical Systems Development with UML, CSDUML (2004), Institut für Informatik, Technische Universität München), 85-99, Technical report TUM-I0415
[20] Calegari, D.; Cengarle, M. V.; Szasz, N., UML 2.0 interactions with OCL/RT constraints, (Proc. Forum on Specification and Design Languages. Proc. Forum on Specification and Design Languages, FDL (2008)), 167-172
[21] Alur, R.; Holzmann, G. J.; Peled, D., An analyser for message sequence charts, (Proc. Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop. Proc. Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS’96. Proc. Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop. Proc. Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS’96, LNCS, vol. 1055 (1996), Springer), 35-48
[22] Alur, R.; Etessami, K.; Yannakakis, M., Inference of message sequence charts, IEEE Trans. Softw. Eng., 29, 7, 623-633 (2003)
[23] Zheng, T.; Khendek, F.; Hélouët, L., A semantics for timed MSC, Electron. Notes Theor. Comput. Sci., 65, 7 (2002) · Zbl 1268.68118
[24] Damm, W.; Harel, D., LSCs: breathing life into message sequence charts, Form. Methods Syst. Des., 19, 1, 45-80 (2001) · Zbl 0985.68033
[25] Harel, D.; Marelly, R., Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine (2003), Springer
[26] Harel, D.; Thiagarajan, P. S., Message sequence charts, (UML for Real: Design of Embedded Real-Time Systems (2003), Kluwer Academic Publishers), 77-105
[27] Faltin, N.; Lambert, L.; Mitschele-Thiel, A.; Slomka, F., An annotational extension of message sequence charts to support performance engineering, (SDL’97, Time for Testing. SDL’97, Time for Testing, SDL Forum (1997), Elsevier), 307-322
[28] Lambert, L., PMSC for performance evaluation, (Proc. 1. Workshop on Performance and Time in SDL/MSC (1998)), 70-80
[31] Abdulatif, A. A.; Pooley, R., A computer assisted state marking method for extracting performance models from design models, Int. J. Simul. Syst. Sci. Technol., 36-46 (September 2007)
[32] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall · Zbl 0637.68007
[33] Seidel, K., Probabilistic communicating processes, Theor. Comput. Sci., 152, 2, 219-249 (1995) · Zbl 0872.68111
[34] McIver, A.; Morgan, C., Abstraction, Refinement and Proof for Probabilistic Systems (2005), Springer · Zbl 1069.68039
[35] McIver, A.; Morgan, C., Developing and reasoning about probabilistic programs in pGCL, (Proc. First Pernambuco Summer School on Software Engineering, Revised Lectures. Proc. First Pernambuco Summer School on Software Engineering, Revised Lectures, PSSE. Proc. First Pernambuco Summer School on Software Engineering, Revised Lectures. Proc. First Pernambuco Summer School on Software Engineering, Revised Lectures, PSSE, LNCS, vol. 3167 (2006), Springer), 123-155
[36] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall · Zbl 0286.00013
[37] Hehner, E. C.R., Probabilistic predicative programming, (Proc. 7th International Conference on Mathematics of Program Construction. Proc. 7th International Conference on Mathematics of Program Construction, LNCS, vol. 3125 (2004), Springer), 169-185 · Zbl 1106.68341
[38] Segala, R., Modeling and verification of randomized distributed real-time systems (1995), Massachusetts Institute of Technology, PhD thesis
[39] Segala, R.; Lynch, N., Probabilistic simulations for probabilistic processes, Nord. J. Comput., 2, 2, 250-273 (1995) · Zbl 0839.68067
[40] de Alfaro, L.; Henzinger, T. A.; Jhala, R., Compositional methods for probabilistic systems, (Proc. 12th International Conference on Concurrency Theory. Proc. 12th International Conference on Concurrency Theory, CONCUR (2001), Springer), 351-365 · Zbl 1006.68083
[41] Jonsson, B.; Larsen, K. G., Specification and refinement of probabilistic processes, (Proc. 6th Annual IEEE Symposium on Logic in Computer Science (1991)), 266-277
[42] Jonsson, B.; Ho-Stuart, C.; Yi, W., Testing and refinement for nondeterministic and probabilistic processes, (Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 863 (1994), Springer), 418-430
[43] Jonsson, B.; Yi, W., Compositional testing preorders for probabilistic processes, (Proc. 10th Annual IEEE Symposium on Logic in Computer Science (1995), IEEE Computer Society), 431-443
[44] Broy, M.; Stølen, K., Specification and Development of Interactive Systems: FOCUS on Streams, Interfaces, and Refinement, Monographs in Computer Science (2001), Springer · Zbl 0981.68115
[45] Runde, R. K.; Haugen, Ø.; Stølen, K., How to transform UML neg into a useful construct, (Proc. Norsk Informatikkonferanse (2005), Tapir), 55-66
[46] Refsdal, A.; Runde, R. K.; Stølen, K., Relating computer systems to sequence diagrams with underspecification, inherent nondeterminism and probabilistic choice, Part 2 (2007), Department of Informatics, University of Oslo, Technical Report 347
[47] Dudley, R. M., Real Analysis and Probability, Cambridge Studies in Advanced Mathematics (2002), Cambridge · Zbl 1023.60001
[48] Refsdal, A.; Runde, R. K.; Stølen, K., Stepwise refinement of sequence diagrams with soft real-time requirements (2011), SINTEF ICT, Technical Report A19749
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.