[1] |
Micskei Z, Waeselynck H. The many meanings of UML 2 sequence diagrams: A survey. <i>Software & Systems Modeling</i>, 2011, 10(4): 489-514. DOI: 10.1007/s10270-010-0157-9.
|
|
<br>[2] Pickin S, Jézéquel J M. Using UML sequence diagrams as the basis for a formal test description language. In <i>Proc. the 4th International Conference on Integrated Formal Methods</i>, April 2004, pp.481-500. DOI: 10.1007/978-3-540-24756-2_26.
|
|
<br>[3] Störrle H. Trace semantics of interactions in UML 2.0. <i>J. Visual Languages and Computing</i>, 2004.
|
|
<br>[4] Lund M S. Operational analysis of sequence diagram specifications [Ph.D. Thesis]. University of Oslo, 2008.
|
|
<br>[5] André P, Rivière N, Waeselynck H. A Toolset for mobile systems testing. In <i>Proc. the 11th International Conference on Verification and Evaluation of Computer and Communication Systems</i>, August 2017, pp.124-138. DOI: 10.1007/978-3-319-66176-6_9.
|
|
<br>[6] Mahe E, Gaston C, Gall P L. Revisiting semantics of interactions for trace validity analysis. In <i>Proc. the 23rd International Conference on Fundamental Approaches to Software Engineering</i>, April 2020, pp.482-501. DOI: 10.1007/978-3-030-45234-6_24.
|
|
<br>[7] Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. A causal semantics for UML 2.0 sequence diagrams with nested combined fragments. In <i>Proc. the 12th International Conference on Evaluation of Novel Approaches to Software Engineering</i>, April 2017, pp.28-29. DOI: 10.5220/0006314100470056.
|
|
<br>[8] Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. An operational semantics of UML 2.X sequence diagrams for distributed systems. In <i>Proc. the 12th International Conference on Evaluation of Novel Approaches to Software Engineering</i>, April 2018, pp.158-182. DOI: 10.1007/978-3-319-94135-6_8.
|
|
<br>[9] Dhaou F, Mouakher I, Attiogbé J C, Bsaies K. Guard evaluation and synchronization issues in causal semantics for UML 2.X sequence diagrams. In <i>Proc. the 13th Int. Conference on Evaluation of Novel Approaches to Software Engineering</i>, March 2018, pp.275-282. DOI: 10.5220/0006708102750282.
|
|
<br>[10] Abrial J R. Modeling in Event-B---System and Software Engineering. Cambridge University Press, 2010.
|
|
<br>[11] Abrial J R, Butler M, Hallerstede S, Hoang T S, Mehta F, Voisin L. Rodin: An open toolset for modelling and reasoning in Event-B. <i>Int. J. Softw. Tools Technol. Transf.</i>, 2010, 12(6): 447-466. DOI: 10.1007/s10009-010-0145-y.
|
|
<br>[12] Leuschel M, Butler M. ProB: An Automated analysis toolset for the B Method. <i>Int. J. Softw. Tools Technol. Transf.</i>, Springer-Verlag, 2008, 10(2): 185-203. DOI: 10.1007/s10009-007-0063-9.
|
|
<br>[13] Boulanger J L. Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, 2014. DOI: 10.1002/9781119002727.
|
|
<br>[14] Rasch H, Wehrheim H. Checking the validity of scenarios in UML models. In <i>Proc. the 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems</i>, June 2005, pp.67-82. DOI: 10.1007/11494881_5.
|
|
<br>[15] Knapp A, Wuttke J. Model checking of UML 2.0 interactions. In <i>Proc. the Workshops and Symposia at 2016 International Conference on Model Driven Engineering Languages and Systems</i>, October 2007, pp.42-51. DOI: 10.1007/978-3-540-69489-2_6.
|
|
<br>[16] Lima V, Talhi C, Mouheb D, Debbabi M, Wang L, Pourzandi M. Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. <i>Electron. Notes Theor. Comput. Sci.</i>, 2009, 254: 143-160. DOI: 10.1016/j.entcs.2009.09.064.
|
|
<br>[17] Cunha E, Custodio M, Rocha H, Barreto R. Formal verification of UML sequence diagrams in the embedded systems context. In <i>Proc. the 2011 Brazilian Symposium on Computing System Engineering</i>, November 2011, pp.39-45. DOI: 10.1109/SBESC.2011.18.
|
|
<br>[18] Zhu M, Wang H, Liu X, Han X. Formal analysis of sequence diagram with time constraints by model transformation. <i>Int. J. Softw. Informatics</i>, 2012, 6(2): 327-357.
|
|
<br>[19] Miyazaki H, Yokogawa T, Amasaki S, Asada K, Sato Y. Synthesis and refinement check of sequence diagrams. <i>IEICE Transactions on Information & Systems</i>, 2012, E95-D(9): 2193-2201. DOI: 10.1587/transinf.E95.D.2193.
|
|
<br>[20] Remenska D, Willemse T A C, Templon J, Verstoep K, Bal H E. Property specification made easy: Harnessing the power of model checking in UML designs. In <i>Proc. the 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems</i>, June 2014, pp.17-32. DOI: 10.1007/978-3-662-43613-4_2.
|
|
<br>[21] Muram F U, Tran H, Zdun U. Supporting automated containment checking of software behavioural models using model transformations and model checking. <i>Science of Computer Programming</i>, 2019, 174: 38-71. DOI: 10.1016/j.scico.2019.01.005.
|
|
<br>[22] Lima L, Miyazawa A, Cavalcanti A, Cornélio M, Iyoda J, Sampaio A, Hains R, Larkham A, Lewis V. An integrated semantics for reasoning about SysML design models using refinement. <i>Software & Systems Modeling</i>, 2017, 16(3): 875-902. DOI: 10.1007/s10270-015-0492-y.
|
|
<br>[23] Pan M, Chen S, Pei Y, Zhang T, Li X. Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In <i>Proc. the 41st IEEE/ACM International Conference on Software Engineering</i>, May 2019, pp.212-222. DOI: 10.1109/ICSE.2019.00037.
|
|
<br>[24] Chen X, Mallet F, Liu X. Formally verifying sequence diagrams for safety critical systems. In <i>Proc. the 14th Int. Symposium on Theoretical Aspects of Software Engineering</i>, December 2020, pp.217-224. DOI: 10.1109/TASE49443.2020.00037.
|
|
<br>[25] Alur R, Holzmann G J, Peled D. An analyzer for message sequence charts. In <i>Proc. the 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems</i>, March 1996, pp.35-48. DOI: 10.1007/3-540-61042-1_37.
|
|
<br>[26] Tahir O, Sibertin-Blanc C, Cardoso J. A causality-based semantics for UML sequence diagrams. In <i>Proc. IASTED Int. Conference on Software Engineering</i>, February 2005, pp.106-111.
|
|
<br>[27] Damchoom K, Butler M, Abrial J R. Modelling and proof of a tree-structured file system in Event-B and Rodin. In <i>Proc. the 10th International Conference on Formal Engineering Methods</i>, October 2008, pp.25-44. DOI: 10.1007/978-3-540-88194-0_5.
|
|
<br>[28] Mouakher I. Case study for sequence diagram transformation in Event-B. Technical Report, 2021.https://www.dropbox.com/s/8oeuy4gwfsa8cqh/mainTR.pdf?dl=0.
|