{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T03:53:45Z","timestamp":1648526025903},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Having a sequence diagram specification and a computer system, we need to answer the question: Is the system compliant with the sequence diagram specification in the desired way? We present a procedure for answering this question for sequence diagrams with underspecification and inherent nondeterminism. The procedure is independent of any concrete technology, and relies only on the execution traces that may be produced by the system. If all traces are known, the procedure results in either \u201ccompliant\u201d or \u201cnot compliant\u201d. If only a subset of the traces is known, the conclusion may also be \u201clikely compliant\u201d or \u201clikely not compliant\u201d.<\/jats:p>","DOI":"10.1007\/s00165-011-0192-5","type":"journal-article","created":{"date-parts":[[2011,8,13]],"date-time":"2011-08-13T06:18:31Z","timestamp":1313216311000},"page":"159-187","source":"Crossref","is-referenced-by-count":4,"title":["Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism"],"prefix":"10.1145","volume":"25","author":[{"given":"Ragnhild Kobro","family":"Runde","sequence":"first","affiliation":[{"name":"Department of Informatics, University of Oslo, PO Box 1080, Blindern, 0316, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atle","family":"Refsdal","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo, PO Box 1080, Blindern, 0316, Oslo, Norway"},{"name":"SINTEF ICT, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ketil","family":"St\u00f8len","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo, PO Box 1080, Blindern, 0316, Oslo, Norway"},{"name":"SINTEF ICT, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bowles JKF (2006) Decomposing interactions. In: Algebraic methodology and software technology (AMAST 2006). LNCS vol 4019. Springer Berlin pp 189\u2013203","DOI":"10.1007\/11784180_16"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Broy M St\u00f8len K (2001) Specification and development of interactive systems: FOCUS on streams interfaces and refinement. Springer Berlin","DOI":"10.1007\/978-1-4613-0091-5"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Cavarra A Filipe JK (2004) Formalizing liveness-enriched sequence diagrams using ASMs. In: Abstract state machines (ASM 2004). LNCS vol 3052. Springer Berlin pp 62\u201377","DOI":"10.1007\/978-3-540-24773-9_6"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/2773580.2773785"},{"key":"e_1_2_1_2_7_2","unstructured":"Cengarle MV Knapp A (2004) UML 2.0 interactions: semantics and refinement. In: Proceedings 3rd international workshop on critical systems development with UML (CSDUML\u201904). Technical report TUM-I0415. Institut f\u00fcr Informatik Technische Universit\u00e4t M\u00fcnchen pp 85\u201399"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.068"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Gaudel M-C (1995) Testing can be formal too. In: Theory and practice of software development (TAPSOFT\u201995). LNCS vol 915. Springer Berlin pp 82\u201396","DOI":"10.1007\/3-540-59293-8_188"},{"key":"e_1_2_1_2_11_2","unstructured":"Grosu R Smolka SA (2005) Safety-liveness semantics for UML 2.0 sequence diagrams. In: Proceedings applications of concurrency to system design (ACSD\u201905). IEEE Computer Society pp 6\u201314"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-005-0087-0"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Harel D Marelly R (2003) Come let\u2019s play: scenario-based programming using LSCs and the play-engine. Springer Berlin","DOI":"10.1007\/978-3-642-19029-2"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-007-0054-z"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Haugen \u00d8 St\u00f8len K (2003) STAIRS\u2014steps to analyze interactions with refinement semantics. In: The unified modeling language. Modeling languages and applications (UML 2003). LNCS vol 2863. Springer Berlin pp 388\u2013402","DOI":"10.1007\/978-3-540-45221-8_33"},{"key":"e_1_2_1_2_17_2","unstructured":"International Standards Organization (1989) Information processing systems\u2014open systems interconnection\u2014LOTOS\u2014a formal description technique based on the temporal ordering of observational behaviour\u2014ISO 8807"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Jacob J (1989) On the derivation of secure components. In: Proceedings of the IEEE symposium on security and privacy pp 242\u2013247","DOI":"10.1109\/SECPRI.1989.36298"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:EMSE.0000013513.48963.1b"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2001) Secrecy-preserving refinement. In: Formal methods for increasing software productivity (FME 2001). LNCS vol 2021. Springer Berlin pp 135\u2013152","DOI":"10.1007\/3-540-45251-6_8"},{"key":"e_1_2_1_2_21_2","unstructured":"Kr\u00fcger IH (2000) Distributed system design with message sequence charts. PhD thesis. Technische Universit\u00e4t M\u00fcnchen"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Knapp A Wuttke J (2007) Model checking of UML 2.0 interactions. In: Models in software engineering. LNCS vol 4364. Springer Berlin pp 42\u201351","DOI":"10.1007\/978-3-540-69489-2_6"},{"key":"e_1_2_1_2_23_2","unstructured":"Larsen PG Arentoft MM Monahan BQ Bear S (1989) Towards a formal semantics of the BSI\/VDM specification language. In: Information processing 89: proceedings IFIP 11th world computer congress. Elsevier Amsterdam pp 95\u2013100"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Lund MS Refsdal A St\u00f8len K (2010) Semantics of UML models for dynamic behavior. A survey of different approaches. In: Model-based engineering of embedded real-time systems. LNCS vol 6100. Springer Berlin pp 77\u2013103","DOI":"10.1007\/978-3-642-16277-0_4"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Lund MS St\u00f8len K (2006) Deriving tests from UML 2.0 sequence diagrams with neg and assert. In: Proceedings 1st international workshop on automation of software test (AST\u201906). ACM Press pp 22\u201328","DOI":"10.1145\/1138929.1138934"},{"key":"e_1_2_1_2_26_2","unstructured":"Lund MS (2008) Operational analysis of sequence diagram specifications. PhD thesis University of Oslo"},{"issue":"1","key":"e_1_2_1_2_27_2","first-page":"117","article-title":"Model-based testing with the escalator tool","volume":"105","author":"Lund MS","year":"2009","journal-title":"Telektronikk"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Micskei Z Waeselynck H (2010) The many meanings of UML 2 sequence diagrams: a survey. Softw Syst Model (Online First) 1\u201326","DOI":"10.1007\/s10270-010-0157-9"},{"key":"e_1_2_1_2_30_2","unstructured":"Object Management Group (2006) Object constraint language 2.0 document: formal\/2006-05-01 edition"},{"key":"e_1_2_1_2_31_2","unstructured":"Object Management Group (2010) UML 2.3 superstructure specification document: formal\/2010-05-05 edition"},{"key":"e_1_2_1_2_32_2","unstructured":"Runde RK Haugen \u00d8 St\u00f8len K (2005) How to transform UML neg into a useful construct. In: Proceedings Norsk Informatikkonferanse (NIK 2005) Tapir pp 55\u201366"},{"issue":"2","key":"e_1_2_1_2_33_2","first-page":"157","article-title":"Refining UML interactions with underspecification and nondeterminism","volume":"12","author":"Runde RK","year":"2005","journal-title":"Nordic J Comput"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Roscoe B (1995) CSP and determinism in security modelling. In: Proceedings 1995 IEEE symposium on security and privacy. IEEE Computer Society Press pp 114\u2013127","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"e_1_2_1_2_35_2","unstructured":"Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall"},{"key":"e_1_2_1_2_36_2","unstructured":"Runde RK Refsdal A St\u00f8len K (2007) Relating computer systems to sequence diagrams with underspecification inherent nondeterminism and probabilistic choice. Part 2: probabilistic choice. Technical report 347 Department of Informatics University of Oslo"},{"key":"e_1_2_1_2_37_2","unstructured":"Runde RK Refsdal A St\u00f8len K (2011) Relating computer systems to sequence diagrams\u2014the impact of underspecification and inherent nondeterminism. Technical report 410 Department of Informatics University of Oslo"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Steen M Bowman H Derrick J and Boiten E (1997) Disjunction of LOTOS specifications. In: Formal description techniques and protocol specification testing and verification (FORTE X\/PSTV XVII \u201997). Chapman & Hall pp 177\u2013192","DOI":"10.1007\/978-0-387-35271-8_11"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.82"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Seehusen F St\u00f8len K (2006) Information flow property preserving transformation of UML interaction diagrams. In: Proceedings symposium on access control models and technologies (SACMAT 2006). ACM New York pp 150\u2013159","DOI":"10.1145\/1133058.1133080"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-008-0102-3"},{"key":"e_1_2_1_2_42_2","unstructured":"St\u00f6rrle H (2003) Assert negate and refinement in UML-2 interactions. In: Proceedings 2nd international workshop on critical systems development with UML (CSDUML\u201903). Technical report TUM-I0317 Institut f\u00fcr Informatik Technische Universit\u00e4t M\u00fcnchen pp 79\u201393"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Tretmans J (1999) Testing concurrent systems: a formal approach. In: Proceedings 10th international conference on concurrency theory (CONCUR\u201999). LNCS vol 1664. Springer Berlin pp 46\u201365","DOI":"10.1007\/3-540-48320-9_6"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Uchitel S Brunet G Chechik M (2007) Behaviour model synthesis from properties and scenarios. In: Proceedings 29th international conference in software engineering (ISCE\u201907). IEEE Computer Society pp 34\u201343","DOI":"10.1109\/ICSE.2007.21"},{"key":"e_1_2_1_2_45_2","unstructured":"Walicki M Meldal S (2001) Nondeterminism vs. underspecification. In: Proceedings systemics cybernetics and informatics (ISAS-SCI 2001). IIIS pp 551\u2013555"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0192-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0192-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0192-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:54:36Z","timestamp":1641484476000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0192-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["10.1007\/s00165-011-0192-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0192-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3]]}}}