{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:29Z","timestamp":1694623949523},"reference-count":11,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1995,9,1]],"date-time":"1995-09-01T00:00:00Z","timestamp":809913600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Assume that a real-time program\n            <jats:italic>P<\/jats:italic>\n            <jats:sup>T<\/jats:sup>\n            consisting of a number of parallel processes is executed on a system having a set\n            <jats:italic>Pr<\/jats:italic>\n            of processors which are shared between the processes by a real-time scheduler\n            <jats:italic>S<\/jats:italic>\n            <jats:sup>T<\/jats:sup>\n            . Assume that P\n            <jats:sup>T<\/jats:sup>\n            must meet some timing deadlines. We show that such an implementation of\n            <jats:italic>P<\/jats:italic>\n            <jats:sup>T<\/jats:sup>\n            can be represented as a transformationL(\n            <jats:italic>P<\/jats:italic>\n            <jats:sup>T<\/jats:sup>\n            ) and that the deadlines of\n            <jats:italic>P<\/jats:italic>\n            <jats:sup>T<\/jats:sup>\n            will be met if they are satisfied by the timing properties of the transformed program. The condition for feasibility of a real-time program executed under a scheduler is formalized and rules are provided for verification. The scheduler\n            <jats:italic>S<\/jats:italic>\n            <jats:sup>T<\/jats:sup>\n            can be specified\n            <jats:italic>generically<\/jats:italic>\n            and applied to different programs, making it unnecessary to introduce low-level operations such as scheduling primitives into the programming language. Thus real-time program specification and Schedulability can be considered in the same framework and the timing properties of a program can be determined at the specification level. By separating the specification of the scheduler from that of the program, the feasibility of an implementation can be proved by considering a scheduling policy rather than its implementation details.\n          <\/jats:p>","DOI":"10.1007\/bf01211630","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T13:02:46Z","timestamp":1109336566000},"page":"510-532","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verification of schedulability for real-time programs"],"prefix":"10.1145","volume":"7","author":[{"given":"Zhiming","family":"Liu","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Leicester, University Road, LE1 7RH, Leicester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathai","family":"Joseph","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Warwick, Coventry, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomasz","family":"Janowski","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Warwick, Coventry, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Audsley N. Burns A. Richardson M. Tindell K. and Wellings A.: Applying new scheduling theory to static priority pre-emptive scheduling. Technical Report RTRG\/92\/120 Department of Computer Science University of York 1992.","DOI":"10.1049\/sej.1993.0034"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abadi M. and Lamport L.: The existence of refinement mappings. Theoretical Computer Science 82(2) May 1991.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abadi M. and Lamport L.: An old-fashioned recipe for real-time. In W.R. de Rover J.W. de Bakker C. Huizing and G. Rozenberg editors Real-Time: Theory in Practice Lecture Notes in Computer Science 600. Springer-Verlag 1991.","DOI":"10.1007\/BFb0031985"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Henzinger T. Manna Z. and Pnueli A.: Temporal proof methodologies for real-time systems. In Proceedings of the 8th ACM Annual Symposium on Principles of Programming Languages pages 269\u2013276 1991.","DOI":"10.1145\/99583.99629"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Hooman J.: A denotational real-time semantics for shared processors. In PARLE'91 Parallel Architectures and Languages Europe Vol. II Lecture Notes in Computer Science 506 pages 185\u2013201. Springer-Verlag 1991.","DOI":"10.1007\/3-540-54152-7_65"},{"key":"e_1_2_1_2_6_2","volume-title":"Technical report","author":"Lamport L.","year":"1990"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Liu Z. and Joseph M.: Specification and verification of recovery in asynchronous communicating systems. In J. Vytopil editor Formal Techniques in Real-Time and Fault Tolerant Systems pages 137\u2013166. Kluwer Academic Publishers 1993.","DOI":"10.1007\/978-1-4615-3220-0_6"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Liu Z. and Joseph M.: Stepwise development of fault-tolerant reactive systems. In H. Langmaak W.-P. de Roever and J. Vytopil editors Formal Techniques in Real-Time and Fault Tolerant Systems Lecture Notes in Computer Science 863 pages 529\u2013546. Springer-Verlag 1994.","DOI":"10.1007\/3-540-58468-4_182"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Zhou C.C. Hoare C.A.R. and Ravn A.P.: A calculus of durations. Information Processing Letters 40(5) December 1991.","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_2_10_2","unstructured":"Zhou C.C. Hansen M.R. Ravn A.P. and Rischel H.: Duration specifications for shared processors. In J. Vytopil editor Formal Techniques in Real-Time and Fault-Tolerant Systems Lecture Notes in Computer Science 571 . Springer-Verlag January 1992."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Zhang Y. and Zhou C.C.: A formal proof of the deadline driven scheduler. In H. Langmaak W.-P. de Roever and J. Vytopil editors Formal Techniques in Real-Time and Fault Tolerant Systems Lecture Notes in Computer Science 863 pages 756\u2013775. Springer-Verlag 1994.","DOI":"10.1007\/3-540-58468-4_194"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211630.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211630\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211630","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:28:57Z","timestamp":1641482937000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211630"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,9]]},"references-count":11,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1995,9]]}},"alternative-id":["10.1007\/BF01211630"],"URL":"https:\/\/doi.org\/10.1007\/bf01211630","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,9]]}}}