{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:28:27Z","timestamp":1694618907655},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"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":[[2000,10]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            This paper introduces and motivates ADL, a new formal notation for the specification of the temporal and functional behaviour of concurrent processes. ADL is tailored to be directly compatible with the DORIS design method. It combines a graphical\n            <jats:italic>Activity State-Machine<\/jats:italic>\n            (ASM) notation and a model-based\n            <jats:italic>Activity Functional Behaviour<\/jats:italic>\n            (AFB) notation. The abstract syntax, and static and dynamic semantics for the ASM notation are given, the dynamic semantics being given proof-theoretically in many-sorted logic extended with the RTL \u2018occurrence\u2019 relation,\n            <jats:italic>\u0398<\/jats:italic>\n            , and the ERTL \u2018holding\u2019 relation,\n            <jats:italic>\u03a6<\/jats:italic>\n            . ADL is used to specify a small network, and proofs are given of its timeliness and safety properties.\n          <\/jats:p>","DOI":"10.1007\/s001650070032","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T06:34:23Z","timestamp":1030257263000},"page":"120-144","source":"Crossref","is-referenced-by-count":6,"title":["ADL: An Activity Description Language for Real-Time Networks"],"prefix":"10.1145","volume":"12","author":[{"given":"Stephen","family":"Paynter","sequence":"first","affiliation":[{"name":"Matra BAe Dynamics (UK) Ltd, Filton, Bristol, UK, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Armstrong","sequence":"additional","affiliation":[{"name":"Flour Global Services Consulting, Farnham, UK, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Haveman","sequence":"additional","affiliation":[{"name":"Motorola Worldwide Smartcard Solutions Division, UK, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","first-page":"414","volume-title":"5th IEEE Symp. on Logic in Comp. Sci., IEEE Comp. Soc. Press","author":"Alur R.","year":"1990"},{"issue":"2","key":"p_2","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/BF00360339","article-title":"\u2018Specification and Verification of Reactive System Behaviour: The Railroad Crossing Example\u2019","volume":"10","author":"Ar","year":"1996","journal-title":"J. Real-Time Systems"},{"key":"p_3","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/S0164-1212(97)00168-4","article-title":"\u2018Industrial Integration of Graphical Formal Specifications\u2019","volume":"40","author":"Arm","year":"1998","journal-title":"J. Systems Software"},{"issue":"5","key":"p_4","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1049\/sej.1993.0034","article-title":"\u2018Applying New Scheduling Theory to Static Priority Pre-emptive Scheduling\u2019","volume":"8","author":"Audsley N.","year":"1993","journal-title":"Software Engineering Journal"},{"key":"p_5","volume-title":"\u2018High Integrity Ada: The SPARK Approach","author":"Bar","year":"1997"},{"issue":"6","key":"p_6","article-title":"\u2018Formal Methods: Use and Relevance for the Development of Safety Critical Systems\u2019","volume":"35","author":"Ba","year":"1992","journal-title":"Computer Journal"},{"key":"p_7","volume-title":"FACIT","author":"Bicarregui J. C.","year":"1994"},{"key":"p_8","volume-title":"7th Safety-Critical Systems Symp., Huntingdon, In \u2018Towards System Safety\u2019, Edited by F. Redmill and T. Anderson","author":"Bienm\u00fcller T.","year":"1999"},{"key":"p_9","volume-title":"BSc Student Project Report, Department of Computing Science","author":"Bou","year":"1999"},{"key":"p_10","volume-title":"3rd Int. Symp. of Formal Methods Europe, LNCS 1051","author":"Brooks T.","year":"1996"},{"key":"p_11","first-page":"225","volume-title":"\u2018Preemptive Priority-Based Scheduling: An Appropriate Engineering Approach","author":"Bur","year":"1995"},{"issue":"2","key":"p_12","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00365316","article-title":"\u2018Combining Static Worst-Case Timing Analysis and Program Proof\u2019","volume":"11","author":"Chapman R.","year":"1996","journal-title":"Journal of Real-Time Systems"},{"key":"p_13","volume-title":"\u2018Applications of Formal Methods","author":"Fitzgerald J. S.","year":"1995"},{"key":"p_14","volume-title":"Proc. of the IEEE EuroMirco'96 Conf.","author":"Ha","year":"1996"},{"key":"p_15","volume-title":"BSc Student Project Report, Department of Computing Science","author":"Hen","year":"1998"},{"key":"p_16","volume-title":"LNCS 558","author":"Hoo","year":"1991"},{"key":"p_17","volume-title":"VDM-SL","author":"International Standards Organisation","year":"1996"},{"issue":"9","key":"p_18","first-page":"890","article-title":"\u2018Safety Analysis of Timing Properties in Real-Time Systems\u2019","volume":"12","author":"Ja","year":"1986","journal-title":"IEEE Transactions"},{"key":"p_19","volume-title":"Crown Copyright","author":"[JIM87] Joint IECCA and MUF Committee on MASCOT (JIMCOM)","year":"1987"},{"key":"p_20","volume-title":"IEEE Proceedings of the 21st Annual Hawaiian International Conference on System Science","author":"Jahanian F.","year":"1988"},{"key":"p_22","volume-title":"\u2018Systematic Software Development Using VDM","author":"Jon","year":"1990"},{"issue":"4","key":"p_23","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/BF01211297","article-title":"\u2018Limits of Formal Methods\u2019","volume":"9","author":"Kne","year":"1997","journal-title":"Formal Aspects of Computing"},{"key":"p_25","volume-title":"\u2018Symbolic Model Checking","author":"Mc","year":"1993"},{"key":"p_26","volume-title":"\u2018The Temporal Logic of Reactive and Concurrent Systems","author":"Ma","year":"1992"},{"key":"p_27","volume-title":"\u2018Introduction to Many-Sorted Logic","author":"Man","year":"1993"},{"key":"p_28","volume-title":"Issue","author":"Mo","year":"1985"},{"key":"p_29","volume-title":"Sea Systems Controllerate: \u2018Requirements for Software for use with Digital Processors","author":"Mo","year":"1991"},{"key":"p_30","volume-title":"Defence Standard 00-55: \u2018The Procurement of Safety-Critical Software in Defence Equipment","author":"Mo","year":"1997"},{"key":"p_31","volume-title":"SRI International","author":"Owre S.","year":"1999"},{"key":"p_32","volume-title":"SRI International","author":"Owre S.","year":"1999"},{"key":"p_36","volume-title":"Proc. of the Int. Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571","author":"Sc","year":"1992"},{"issue":"3","key":"p_37","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1049\/sej.1986.0018","article-title":"\u2018The MASCOT Method\u2019","volume":"1","author":"Sim","year":"1986","journal-title":"Software Engineering Journal"},{"key":"p_38","volume-title":"IEE Colloquium on MASCOT and Related Issues.","author":"Sim","year":"1990"},{"key":"p_39","volume-title":"IED Supporting Predictable Implementation of Requirements in Timing and Safety (SPIRITS) Deliverable","author":"Sim","year":"1994"},{"key":"p_40","volume-title":"IEEE Workshop on the Engineering of Computer Based Systems","author":"Sim","year":"1994"},{"key":"p_41","volume-title":"Proc. of the 8th IEEE Symp. on Parallel and Distributed Processing","author":"Sim","year":"1996"},{"issue":"2","key":"p_46","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1049\/sej.1996.0010","article-title":"\u2018Rapier 2000 Software Development Programme\u2019","volume":"11","author":"Woo","year":"1996","journal-title":"Software Engineering Journal"},{"issue":"2","key":"p_47","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01211617","article-title":"\u2018The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs\u2019","volume":"9","author":"Xu Q.","year":"1997","journal-title":"Formal Aspects of Computing"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650070032.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650070032\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650070032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:32:49Z","timestamp":1641483169000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650070032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["10.1007\/s001650070032"],"URL":"https:\/\/doi.org\/10.1007\/s001650070032","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}