{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:57:06Z","timestamp":1762459026527},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2012,7,1]],"date-time":"2012-07-01T00:00:00Z","timestamp":1341100800000},"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":[[2012,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Formal methods are one of the most important approaches to increasing the confidence in the correctness of software systems. A formal specification can be used as an\n            <jats:italic>oracle<\/jats:italic>\n            in testing since one can determine whether an observed behaviour is allowed by the specification. This is an important feature of formal testing: behaviours of the system observed in testing are compared with the specification and ideally this comparison is automated. In this paper we study a formal testing framework to deal with systems that interact with their environment at physically distributed interfaces, called ports, and where choices between different possibilities are probabilistically quantified. Building on previous work, we introduce two families of schedulers to resolve nondeterministic choices among different actions of the system. The first type of schedulers, which we call\n            <jats:italic>global schedulers<\/jats:italic>\n            , resolves nondeterministic choices by representing the environment as a single global scheduler. The second type, which we call\n            <jats:italic>localised schedulers<\/jats:italic>\n            , models the environment as a set of schedulers with there being one scheduler for each port. We formally define the application of schedulers to systems and provide and study different implementation relations in this setting.\n          <\/jats:p>","DOI":"10.1007\/s00165-012-0244-5","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"679-699","source":"Crossref","is-referenced-by-count":8,"title":["Using schedulers to test probabilistic distributed systems"],"prefix":"10.1145","volume":"24","author":[{"given":"Robert M.","family":"Hierons","sequence":"first","affiliation":[{"name":"Department of Information Systems and Computing, Brunel University, UB8 3PH, Uxbridge, Middlesex, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"N\u00fa\u00f1ez","sequence":"additional","affiliation":[{"name":"Departamento de Sistemas Inform\u00e1ticos y Computaci\u00f3n, Universidad Complutense de Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Aldini A Bravetti M (2000) An asynchronous calculus for generative-reactive probalistic systems. In: 8th process algebras and performance modelling workshop PAPM\u201900. Carleton Scientific pp 591\u2013606"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1355340"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00344-9"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Ben-Abdallah H Leue S (1997) Syntactic detection of process divergence and non-local choice in Message Sequence Charts. In: 3rd international workshop on tools and algorithms for construction and analysis of systems TACAS\u201997 LNCS vol 1217. Springer Berlin pp 259\u2013274","DOI":"10.1007\/BFb0035393"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Brinksma E Heerink L Tretmans J (1998) Factorized test generation for multi-input\/output transition systems. In: 11th IFIP workshop on testing of communicating systems IWTCS\u201998. Kluwer Dordrecht pp 67\u201382","DOI":"10.1007\/978-0-387-35381-4_5"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90166-F"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2808"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Christoff I (1990) Testing equivalences and fully abstract models for probabilistic processes. In: 1st international conference on concurrency theory CONCUR\u201990 LNCS vol 458. Springer Berlin pp 126\u2013140","DOI":"10.1007\/BFb0039056"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.033"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(99)00036-1"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Cheung L Stoelinga M Vaandrager F (2007) A testing scenario for probabilistic processes. J ACM 54(6):Article 29","DOI":"10.1145\/1314690.1314693"},{"key":"e_1_2_1_2_12_2","unstructured":"Dssouli R von Bochmann G (1985) Error detection with multiple observers. In: 5th WG6.1 international conference on protocol specification testing and Verification PSTV\u201985. North-Holland Amsterdam pp 483\u2013494"},{"key":"e_1_2_1_2_13_2","unstructured":"Dssouli R von Bochmann G (1986) Conformance testing with multiple observers. In: 6th WG6.1 international conference on protocol specification testing and verification PSTV\u201986. North-Holland Amsterdam pp 217\u2013229"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek R Hennessy M Morgan C Zhang C (2007) Characterising testing preorders for finite probabilistic processes. In: 22nd Annual IEEE symposium on logic in computer science LICS\u201907. IEEE Computer Society pp 313\u2013325","DOI":"10.1109\/LICS.2007.15"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek R Hennessy M Morgan C (2008) Characterising testing preorders for finite probabilistic processes. Logical Methods Comput Sci 4(4)","DOI":"10.2168\/LMCS-4(4:4)2008"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek R Hennessy M Morgan C (2009) Testing finitary probabilistic processes. In: 20th international conference on concurrency theory CONCUR\u201909 LNCS 5710. Springer Berlin pp 274\u2013288","DOI":"10.1007\/978-3-642-04081-8_19"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Deng Y van Glabbeek R Hennessy M Morgan C (2011) Real-reward testing for probabilistic processes (extended abstract). In: 9th workshop on quantitative aspects of programming languages QAPL\u201911 EPTCS 57 pp 61\u201373","DOI":"10.4204\/EPTCS.57.5"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Gaudel M-C (1995) Testing can be formal too! In: 6th International joint conference CAAP\/FASE 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_19_2","doi-asserted-by":"crossref","unstructured":"Giro S D\u2019Argenio PR (2009) On the expressive power of schedulers in distributed probabilistic systems. In: 7th Workshop on quantitative aspects of programming languages QAPL\u201909. Electron Notes Theor Comput Sci 253(3):45\u201371","DOI":"10.1016\/j.entcs.2009.10.005"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Grieskamp W Gurevich Y Schulte W Veanes M (2002) Generating finite state machines from abstract state machines. In: ACM SIGSOFT symposium on software testing and analysis ISSTA\u201902. ACM Press New York pp 112\u2013122","DOI":"10.1145\/566172.566190"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.427"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1123"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Hierons RM Bogdanov K Bowen JP Cleaveland R Derrick J Dick J Gheorghe M Harman M Kapoor K Krause P Luettgen G Simons AJH Vilkomir S Woodward MR Zedan H (2009) Using formal methods to support testing. ACM Comput Surv 41(2)","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Hierons RM Bowen JP Harman M (eds) (2008) Formal methods and testing. In: LNCS vol 4949. Springer Berlin","DOI":"10.1007\/978-3-540-78917-8"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-011-0153-5"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.06.030"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hierons RM Merayo MG N\u00fa\u00f1ez M (2008) Controllable test cases for the distributed test architecture. In: 6th International symposium on automated technology for verification and analysis ATVA\u201908. LNCS vol 5311. Springer Berlin pp 201\u2013215","DOI":"10.1007\/978-3-540-88387-6_16"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Hierons RM Merayo MG N\u00fa\u00f1ez M (2008) Implementation relations for the distributed test architecture. In: Joint 20th IFIP TC6\/WG6.1 international conference on testing of software and communicating systems TestCom\u201908 and 8th international workshop on formal approaches to software testing FATES\u201908. LNCS vol 5047. Springer Berlin pp 200\u2013215","DOI":"10.1007\/978-3-540-68524-1_15"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-011-0149-1"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Hierons RM N\u00fa\u00f1ez M (2010) Testing probabilistic distributed systems. In: IFIP 30th international conference on formal techniques for distributed systems FMOODS\/FORTE\u201910. LNCS vol 6117. Springer Berlin pp 63\u201377","DOI":"10.1007\/978-3-642-13464-7_6"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxm096"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Jard C J\u00e9ron T Kahlouche H Viho C (1998) Towards automatic distribution of testers for distributed conformance testing. In: TC6 WG6.1 joint international conference on formal description techniques and protocol specification testing and verification FORTE\u201998. Kluwer Dordrecht pp 353\u2013368","DOI":"10.1007\/978-0-387-35394-4_22"},{"key":"e_1_2_1_2_33_2","unstructured":"Luo G Dssouli R von Bochmann G (1993) Generating synchronizable test sequences based on finite state machine with distributed ports. In: 6th IFIP workshop on protocol test systems IWPTS\u201993. North-Holland Amsterdam pp 139\u2013153"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.047"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213492"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/95423"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.5555\/983238"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00069-3"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021759127956"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1984.1096074"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Segala R (1995) A compositional trace-based semantics for probabilistic automata. In: 6th international conference on concurrency theory CONCUR\u201995 LNCS vol 962. Springer Berlin pp 234\u2013248.","DOI":"10.1007\/3-540-60218-6_17"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Segala R (1996) Testing probabilistic automata. In: 7th international conference on concurrency theory CONCUR\u201996. LNCS vol 1119. Springer Berlin pp 299\u2013314","DOI":"10.1007\/3-540-61604-7_62"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2652"},{"issue":"2","key":"e_1_2_1_2_48_2","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala R","year":"1995","journal-title":"Nordic J Comput"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Tretmans J (2008) Model based testing with labelled transition systems. In: Formal methods and testing. LNCS vol 4949. Springer Berlin pp 1\u201338","DOI":"10.1007\/978-3-540-78917-8_1"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00364-8"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00056-X"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Yi W Larsen KG (1992) Testing probabilistic and nondeterministic processes. In: 12th IFIP\/WG6.1 international symposium on protocol specification testing and verification PSTV\u201992. North Holland Amsterdam pp 47\u201361","DOI":"10.1016\/B978-0-444-89874-6.50010-6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0244-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0244-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0244-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:01:25Z","timestamp":1641484885000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0244-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":52,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0244-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0244-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}