{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T18:04:53Z","timestamp":1694628293724},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2007,3,1]],"date-time":"2007-03-01T00:00:00Z","timestamp":1172707200000},"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":[[2007,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The complete verification of the timing properties of a large critical system cannot be undertaken in a single step or with a single method. In this paper we present a process that links together a number of techniques and approaches that cover all stages of development from requirements analysis to code testing. The key elements of the process are: a constrained form of timed automata that uses\n            <jats:italic>delay<\/jats:italic>\n            and\n            <jats:italic>deadline<\/jats:italic>\n            to define temporal behaviour, notions of\n            <jats:italic>rely<\/jats:italic>\n            and\n            <jats:italic>guarantee<\/jats:italic>\n            to cover temporal dependencies, model checking for design verification, SPARK and Ravenscar restrictions for programming, and scheduling and response time analysis for asserting implementation compliance. Extended examples of the use of the process are given.\n          <\/jats:p>","DOI":"10.1007\/s00165-006-0021-4","type":"journal-article","created":{"date-parts":[[2006,12,19]],"date-time":"2006-12-19T13:04:55Z","timestamp":1166533495000},"page":"111-136","source":"Crossref","is-referenced-by-count":7,"title":["An engineering process for the verification of real-time systems"],"prefix":"10.1145","volume":"19","author":[{"given":"A.","family":"Burns","sequence":"first","affiliation":[{"name":"Real-Time Systems Research Group, Department of Computer Science, The University of York, YO10 5DD, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T. -M.","family":"Lin","sequence":"additional","affiliation":[{"name":"Real-Time Systems Research Group, Department of Computer Science, The University of York, YO10 5DD, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Alur R Dill D (1990) Automata for modeling real-time systems. In: ICALP 1990 vol 443 of LNCS. Springer Berlin Heidelberg New York; pp 322\u2013335","DOI":"10.1007\/BFb0032042"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA (1992) Logics and models of real-time: a survey. In: Proceedings of REX workshop Lecture Notes in Computer Science Vol. 600 pp 74\u2013106","DOI":"10.1007\/BFb0031988"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Arnold R Mueller F Whalley D (1994) Bounding worst-case instruction cache performance. In: Proceedings 15th IEEE real time systems symposium pp 172\u2013181","DOI":"10.1109\/REAL.1994.342718"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Baker TP (1991) Stack-based scheduling of realtime processes. Real Time Syst 3(1)","DOI":"10.1007\/BF00365393"},{"key":"e_1_2_1_2_5_2","volume-title":"High integrity Ada: the Spark approach","author":"Barnes J","year":"1997"},{"key":"e_1_2_1_2_6_2","volume-title":"High integrity software: the Spark approach to safety and security","author":"Barnes J","year":"2003"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bernat G Colin A Petters SM (2002) WCET analysis of probabilistic hard real\u2013time systems. In: Proceedings of the 23rd real-time systems symposium pp 279\u2013288","DOI":"10.1109\/REAL.2002.1181582"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/34.2.173"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Burns A Lin T-M (2003) Adding temporal annotations and associated verification to Ravenscar profile. In: Ada-Europe 2003 volume 2655 of Lecture Notes in Computer Science. Springer Berlin Heidelberg New York pp 80\u201391","DOI":"10.1007\/3-540-44947-7_5"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Burns A (1999) The Ravenscar profile. ACM Ada Lett XIX(4):49\u201352","DOI":"10.1145\/340396.340450"},{"key":"e_1_2_1_2_11_2","volume-title":"Real-time systems: specification, verification and analysis","author":"Burns A","year":"1996"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/558498"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chapman R Burns A Wellings AJ (1994) Integrated program proof and worst-case timing analysis of SPARK Ada. In: ACM workshop on language compiler and tool support for real-time systems. ACM Press New York","DOI":"10.1145\/192867.192873"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Chapman R (2000) Industrial experience with SPARK. In: ACM SIGAda 2000","DOI":"10.1145\/369264.369270"},{"key":"e_1_2_1_2_15_2","unstructured":"Colin A Petters SM (2003) Experimental evaluation of code properties for WCET analysis. In: Proceedings 24th IEEE real-time systems Symposium"},{"key":"e_1_2_1_2_16_2","unstructured":"Edgar S Burns A (2001) Statistical analysis of WCET for scheduling. In: Proceedings 22nd IEEE real-time systems symposium"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:19990407"},{"issue":"2","key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1137\/0117039","article-title":"Bounds on multiprocessing timing anomalies","volume":"12","author":"Graham RL","year":"1969","journal-title":"SIAM J Appl Math"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.976937"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008140407193"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Healy CA Whalley DB (1995) Integrating the timing analysis of pipelining and instruction caching. In: Proceedings real time systems symposium pp 288\u2013297","DOI":"10.1109\/REAL.1995.495218"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6313045"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Jones CB (1993) Reasoning about interference in an object-based design method. In: FME\u201993 Vol. 670 of LNCS. Springer Berlin Heidelberg New York pp 1\u201318","DOI":"10.1007\/BFb0024634"},{"key":"e_1_2_1_2_24_2","volume-title":"Real-time systems: specification, verification and analysis","author":"Joseph M","year":"1996"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1049\/ip-d.1983.0001"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Klein MH Ralya TA Pollak B Obenza R Harbour MG (1993) A practitioner\u2019s handbook for real-time analysis: a guide to rate monotonic analysis for real-time systems. Kluwer Dordrecht","DOI":"10.1007\/978-1-4615-2796-1"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Kwon J Wellings AJ King S (2002) Ravenscar-Java: a high integrity profile for real-time Java. In: ACM joint Java Grande-ISCOPE conference ACM Press New York pp 131\u2013140","DOI":"10.1145\/583810.583825"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_2_29_2","unstructured":"Liu J-C Lee H-J (1994) Deterministic upperbounds of the worst-case execution times of caches programs. In: Proceedings real time systems symposium pp 182\u2013191"},{"key":"e_1_2_1_2_30_2","unstructured":"Leung A Palem K Pnueli A (1998) TimeC: a time constraint language for ILP processor compilation. In: The 5th Australian conference on parallel and real time systems Springer Berlin Heidelberg New York pp 57\u201371"},{"issue":"1","key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"Larsen KG","year":"1997","journal-title":"Softw Tools for Technol transfer"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-5316(82)90024-4"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.159841"},{"key":"e_1_2_1_2_34_2","unstructured":"Naydich D Guaspari D (1988) Analyzing ravenscar profile tasks by model checking. Technical report Odyssey Reseach Associates TM-98-0034"},{"key":"e_1_2_1_2_35_2","unstructured":"Pettersson P (1999) Modelling and verification of real-time systems using timed automata: theory and practice. PhD thesis Department of Computer Systems Uppsala University"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00571421"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007905003094"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.4.319"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Whysall PJ (1991) Object oriented specification and refinement. PhD Thesis Department of Computer Science The University of York","DOI":"10.1007\/978-1-4471-3756-6_9"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01088834"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0021-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0021-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0021-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:51:31Z","timestamp":1641484291000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0021-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,3]]}},"alternative-id":["10.1007\/s00165-006-0021-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0021-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,3]]}}}