{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:00Z","timestamp":1763468100859,"version":"3.40.4"},"reference-count":97,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,3,1]],"date-time":"2014-03-01T00:00:00Z","timestamp":1393632000000},"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":[[2014,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A very simple model for train stopping is used as a vehicle for investigating how the development of a control system, initially designed in the continuous domain and subsequently discretized, can be captured within a formal development process compatible with standard model based refinement methodologies. Starting with a formalized requirements analysis using KAOS, an abstract model of the continuous system is created in the ASM formalism. This requires extensions of the KAOS and ASM formalisms, capable of dealing with quantities evolving continuously over real time, which are developed. After considering how the continuous system, described as a continuous control system in the state space framework, can be discretized, a discrete control system is created in the state space framework. This is re-expressed in the ASM formalism. The rigorous results on the relationship between continuous and discrete control system models that are needed to establish provable properties of the discretization, then become the ingredients of a retrenchment between continuous and discrete ASM models, and are thus fully integrated into the formal development. The discrete ASM model can then be further refined towards implementation.<\/jats:p>","DOI":"10.1007\/s00165-012-0263-2","type":"journal-article","created":{"date-parts":[[2012,10,20]],"date-time":"2012-10-20T13:56:42Z","timestamp":1350741402000},"page":"319-366","source":"Crossref","is-referenced-by-count":8,"title":["Continuous KAOS, ASM, and formal control system design across the continuous\/discrete modeling interface: a simple train stopping application"],"prefix":"10.1145","volume":"26","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, 3663 Zhongshan Road North, 200062, Shanghai, People\u2019s Republic of China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wen","family":"Su","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, 3663 Zhongshan Road North, 200062, Shanghai, People\u2019s Republic of China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Runlei","family":"Huang","sequence":"additional","affiliation":[{"name":"Alcatel-Lucent Shanghai Bell, 388 Ningqiao Road, Pudong Jinqiao, 201206, Shanghai, People\u2019s Republic of China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Alur R Courcoubetis C Henzinger T Ho P-H (1993) Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Proceedings of workshop on theory of hybrid systems. LNCS vol. 736. Springer Berlin pp. 209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1025"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","DOI":"10.1142\/6262","volume-title":"Dynamic systems and control with applications","author":"Ahmed N","year":"2006"},{"volume-title":"Linear systems","year":"2006","author":"Antsaklis P","key":"e_1_2_1_2_8_2"},{"key":"e_1_2_1_2_9_2","unstructured":"Banach R Model based refinement and the design of retrenchments. Available from [RET]"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Banach R (2010) A deidealisation semantics for KAOS. In: Lencastre M (RE track) (ed) Proceedings of the ACM SAC-10 (RE track). ACM New York pp 267\u2013274","DOI":"10.1145\/1774088.1774146"},{"volume-title":"Introduction to mathematical control theory","year":"1975","author":"Barnett S","key":"e_1_2_1_2_11_2"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.391826"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3431-2","volume-title":"High-integrity system specification and design","author":"Bowen J","year":"1999"},{"volume-title":"Industrial-strength formal methods in practice","year":"1999","author":"Bowen J","key":"e_1_2_1_2_14_2"},{"key":"e_1_2_1_2_15_2","unstructured":"Banach R Jeske C Retrenchment and refinement interworking: the tower theorems. Available from [RET] (Submitted)"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.11.001"},{"key":"e_1_2_1_2_17_2","first-page":"237","article-title":"The ASM refinement method","volume":"15","author":"B\u00f6rger E","year":"2003","journal-title":"FACJ"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.04.002"},{"key":"e_1_2_1_2_19_2","unstructured":"Broenink J (2010) Embedded control software design with formal methods and engineering models. In: BCS-FACS Evening Seminar September 2010"},{"volume-title":"Abstract state machines. A method for high level system design and analysis","year":"2003","author":"B\u00f6rger E","key":"e_1_2_1_2_20_2"},{"key":"e_1_2_1_2_21_2","unstructured":"Butler M Private communication"},{"key":"e_1_2_1_2_22_2","unstructured":"Butler R (1996) NASA Technical Memorandum 110255. An introduction to requirements capture using PVS: specification of a simple autopilot. Technical report"},{"key":"e_1_2_1_2_23_2","unstructured":"Banach R Zhu H Su W Wu X (2012) Continuous ASM and a pacemaker sensing fragment. In: Derrick J Fitzgerald JS Gnesi S Khurshid S Leuschel M Reeves S Riccobene E (eds) Proceedings of the ABZ-12 LNCS vol. 7316. Springer Berlin pp 65\u201378"},{"key":"e_1_2_1_2_24_2","unstructured":"Banach R Zhu H Su W Wu X Moded operation continuous ASM and an approach to pacemaker sensing (Submitted)"},{"key":"e_1_2_1_2_25_2","unstructured":"Cau A Moszkowski B Zedan H Interval temporal logic. http:\/\/www.cse.dmu.ac.uk\/~cau\/papers\/itlhomepage.pdf"},{"key":"e_1_2_1_2_26_2","volume-title":"Ordinary differential equations with applications","author":"Chicone C","year":"2006","edition":"2"},{"key":"e_1_2_1_2_27_2","unstructured":"Clarke F (1987) Optimization and nonsmooth analysis. Soc Ind Math"},{"volume-title":"Nonsmooth analysis and control theory","year":"1997","author":"Clarke F","key":"e_1_2_1_2_28_2"},{"volume-title":"WIFT\u201995: workshop on industrial-strength formal specification techniques.","year":"1995","author":"Crow J","key":"e_1_2_1_2_29_2"},{"key":"e_1_2_1_2_30_2","unstructured":"Cohen J Slissenko A (2008) Implementation of timed abstract state machines with instantaneous actions by machines with delays. Technical Report TR-LACL-2008-2 LACL University of Paris-12"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and Object-Z: Foundations and Advanced Applications","author":"Derrick J","year":"2001"},{"volume-title":"Modern control systems","year":"2010","author":"Dorf R","key":"e_1_2_1_2_32_2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/551579"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Doyen L Henzinger T Raskin J-F (2005) Automatic rectangular refinement of affine hybrid systems. In: Proceedings of FORMATS-05. LNCS vol 3829. Springer Berlin pp 144\u2013161","DOI":"10.1007\/11603009_13"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Dotti F Iliasov A Ribeiro L Romanovsky A (2009) Modal systems: specification refinement and realisation. In: Proceedings of ICFEM-09. LNCS vol 5885. Springer Berlin","DOI":"10.1007\/978-3-642-10373-5_31"},{"volume-title":"Introduction to Hilbert Spaces with Applications","year":"2005","author":"Debnath L","key":"e_1_2_1_2_36_2"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079"},{"volume-title":"The art of control engineering","year":"1997","author":"Dutton K","key":"e_1_2_1_2_38_2"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.09.001"},{"volume-title":"Digital control systems","year":"1996","author":"Franklin G","key":"e_1_2_1_2_40_2"},{"volume-title":"Digital control engineering: analysis and design","year":"2009","author":"Fadali M","key":"e_1_2_1_2_41_2"},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","author":"Gordon M","key":"e_1_2_1_2_42_2"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/52.57887","article-title":"Seven myths of formal methods","volume":"5","author":"Hall J","year":"1990","journal-title":"IEEE Softw"},{"key":"e_1_2_1_2_44_2","first-page":"669","article-title":"Realising the benefits of formal methods","volume":"13","author":"Hall J","year":"2007","journal-title":"JUCS"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer aided design. LNCS vol 1166. Springer Berlin","DOI":"10.1007\/BFb0031814"},{"key":"e_1_2_1_2_46_2","unstructured":"Harrison J (2007) Formalisong basic complex analysis. In: From insight to proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic Grammar and Rhetoric vol 10. University of Bia\u0142ystok pp 151\u2013165"},{"key":"e_1_2_1_2_47_2","unstructured":"He J (1994) From CSP to hybrid systems. In: Roscoe AW (ed) A classical mind essays in honour of C.A.R. Hoare. Prentice-Hall Upper Saddle River. pp 171\u2013189"},{"key":"e_1_2_1_2_48_2","first-page":"607","article-title":"Formal methods for specifying, validating, and verifying requirements","volume":"13","author":"Heitmeyer C","year":"2007","journal-title":"JUCS"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Henzinger T (1996) The theory of hybrid automata. In: Proceedings of the IEEE LICS-96. IEEE New York pp 278\u2013292.http:\/\/mtc.epfl.ch\/~tah\/Publications\/the_theory_of_hybrid_automata.pdf","DOI":"10.1109\/LICS.1996.561342"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.5555\/5509"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511840371"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Henzinger T Kupferman O (1997) From quantity to quality. In: Proceedings of HART-97. LNCS vol 1201. Springer Berlin pp 48\u201362","DOI":"10.1007\/BFb0014712"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Henzinger T Manna Z Pnueli A (1992) What good are digital clocks? In: Proceedings of ICALP-92. LNCS vol 623. Springer Berlin pp 545\u2013558","DOI":"10.1007\/3-540-55719-9_103"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006023127567"},{"key":"e_1_2_1_2_55_2","unstructured":"IEEE Standard 1474. IEEE Standard for Communications-Based Train Control (CBTC) Performance and Functional Requirements: IEEE Std 1474.1-2004; IEEE Standard for User Interface Requirements in Communications-Based Train Control (CBTC) Systems: IEEE Std 1474.2-2003; IEEE Recommended Practice for Communications-Based Train Control (CBTC) System Design and Functional Allocations: IEEE Std 1474.3-2008"},{"key":"e_1_2_1_2_56_2","unstructured":"Jeske C (2005) Algebraic integration of retrenchment and refinement. PhD thesis University of Manchester"},{"key":"e_1_2_1_2_57_2","unstructured":"Kalman R (2005) Opening lecture IFAC World Congress Prague Czech Republic July 4 2005"},{"key":"e_1_2_1_2_58_2","unstructured":"Karlsruhe Interactive Verifier. http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/kiv\/"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Koymans R (1992) Specifying message passing and time-critical systems with temporal logic. LNCS vol 651. Springer Berlin","DOI":"10.1007\/3-540-56283-4"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.5555\/531493"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0897-6","volume-title":"Real and functional analysis","author":"Lang S","year":"1993"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"crossref","unstructured":"Lester D (2007) Topology in PVS: continuous mathematics with applications. In: Rushby J Shankar N (eds) Proceedings of AFM-07. ACM New York","DOI":"10.1145\/1345169.1345171"},{"key":"e_1_2_1_2_63_2","unstructured":"Letier E (2001) Reasoning about agents in goal-oriented requirements engineering. PhD thesis D\u00e9pt. Ing\u00e9nierie Informatique Universit\u00e9 Catholique de Louvain"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"crossref","unstructured":"Loos S Platzer A Nistor L (2011) Adaptive cruise control: hybrid distributed and now formally verified. In: Butler M Schulte S (eds) Proceedings of FM-11. LNCS vol 6664. Springer Berlin pp 42\u201356 [See also: Technical Report CMU-CS-11-107 Carnegie Mellon University (2011)]","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-85529-5","volume-title":"Elementary functional analysis","author":"MacCluer B","year":"2009"},{"key":"e_1_2_1_2_66_2","unstructured":"Maple.http:\/\/www.maplesoft.com.m. Accessed 21 Sep 2012"},{"key":"e_1_2_1_2_67_2","unstructured":"Mathematica.http:\/\/www.wolfram.com.m. Accessed 21 Sep 2012"},{"key":"e_1_2_1_2_68_2","unstructured":"Meynadier J-M Private communication"},{"key":"e_1_2_1_2_69_2","unstructured":"Matoussi A Gervais F Laleau R (2008) A first attempt to express kaos refinement patterns with event-B. In: B\u00f6rger E Butler M Bowen JP Boca P (eds) Proceedings ABZ-08. LNCS vol 5238. Springer Berlin"},{"key":"e_1_2_1_2_70_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511619953","volume-title":"Real-time systems: formal specification and automatic verification","author":"Olderog E-R","year":"2008"},{"volume-title":"Modern control engineering","year":"2008","author":"Ogata K","key":"e_1_2_1_2_71_2"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"crossref","unstructured":"Ouaknine J (2002) Digitsation and Full Abstraction for Dense-Time Model Checking. In: Proceedings of TACAS-02 LNCS. Springer Berlin pp 37\u201351","DOI":"10.1007\/3-540-46002-0_4"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"publisher","DOI":"10.5555\/237778"},{"key":"e_1_2_1_2_74_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn070"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical analysis of hybrid systems: proving theorems for complex dynamics","author":"Platzer A","year":"2010"},{"key":"e_1_2_1_2_76_2","doi-asserted-by":"crossref","unstructured":"Platzer A (2010) Quantified differential dynamic logic for distributed hybrid systems. In: Dawar A Veith H (eds) Proceedings of CSL-10. LNCS vol 6247. Springer Berlin pp 469\u2013483","DOI":"10.1007\/978-3-642-15205-4_36"},{"key":"e_1_2_1_2_77_2","doi-asserted-by":"publisher","DOI":"10.5555\/547639"},{"key":"e_1_2_1_2_78_2","unstructured":"PVS Homepage.http:\/\/pvs.csl.sri.com.m. Accessed 21 Sep 2012"},{"key":"e_1_2_1_2_79_2","doi-asserted-by":"crossref","unstructured":"Pytlak R (1999) Numerical methods for optimal control problems with state constraints. Lecture Notes in Mathematics vol 1707. Springer Berlin","DOI":"10.1007\/BFb0097244"},{"key":"e_1_2_1_2_80_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:TIME.0000016129.97430.c6"},{"key":"e_1_2_1_2_81_2","unstructured":"Retrenchment Homepage.http:\/\/www.cs.man.ac.uk\/retrenchment.t. Accessed 21 Sep 2012"},{"key":"e_1_2_1_2_82_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3655-2","volume-title":"Linear functional analysis","author":"Rynne B","year":"2000"},{"key":"e_1_2_1_2_83_2","doi-asserted-by":"crossref","unstructured":"Su W Abrial J-R Zhu H Huang R (2011) From requirements to development: methodology and example. In: Proceedings of ICFEM-11. LNCS vol 6991. Springer Berlin pp 437\u2013455","DOI":"10.1007\/978-3-642-24559-6_30"},{"key":"e_1_2_1_2_84_2","first-page":"952","article-title":"Verification of ASM refinements using generalized forward simulation","volume":"7","author":"Schellhorn G","year":"2001","journal-title":"JUCS"},{"key":"e_1_2_1_2_85_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.013"},{"key":"e_1_2_1_2_86_2","doi-asserted-by":"publisher","DOI":"10.5555\/286092"},{"volume-title":"Program development by refinement: case studies using the B-Method","year":"1998","author":"Sekerinski E","key":"e_1_2_1_2_87_2"},{"key":"e_1_2_1_2_88_2","doi-asserted-by":"crossref","unstructured":"Stauner T (2002) Discrete-time refinement of hybrid automata. In: Proceedings of HSCC-02. LNCS vol 2289. Springer Berlin pp 144\u2013161","DOI":"10.1007\/3-540-45873-5_32"},{"key":"e_1_2_1_2_89_2","first-page":"1984","article-title":"Simulation of timed abstract state machines with predicate logic model checking","volume":"14","author":"Slissenko A","year":"2008","journal-title":"JUCS"},{"key":"e_1_2_1_2_90_2","doi-asserted-by":"crossref","unstructured":"Su W Yang F Wu X Gou J Zhu H (2011) Formal approaches to mode conversion and positioning for vehicle systems. In: Proceedings of 3rd IEEE international workshop on security aspects of process and services engineering (COMPSAC Workshops). IEEE New York pp 416\u2013421","DOI":"10.1109\/COMPSACW.2011.76"},{"key":"e_1_2_1_2_91_2","doi-asserted-by":"crossref","unstructured":"Sztipanovits J (2011) Model integration and cyber physical systems: a semantics perspective. In: Butler M Schulte S (eds) Proceedings of FM-11. LNCS vol 6664. Springer Berlin.http:\/\/sites.lero.ie\/download.aspx?f=Sztipanovits-Keynote.pdff [Invited talk FM 2011 Limerick Ireland]","DOI":"10.1007\/978-3-642-21437-0_1"},{"key":"e_1_2_1_2_92_2","doi-asserted-by":"publisher","DOI":"10.5555\/1717907"},{"volume-title":"Requirements engineering: from system goals to uml models to software specifications","year":"2009","author":"van Lamsweerde A","key":"e_1_2_1_2_93_2"},{"key":"e_1_2_1_2_94_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0601-9","volume-title":"Ordinary differential equations","author":"Walter W","year":"1998"},{"volume-title":"Using Z, specification, refinement and proof","year":"1996","author":"Woodcock J","key":"e_1_2_1_2_95_2"},{"key":"e_1_2_1_2_96_2","unstructured":"Willems J (2007) Open dynamical systems: their aims and their origins. Ruberti Lecture Rome. http:\/\/homes.esat.kuleuven.be\/~jwillems\/Lectures\/2007\/Rubertilecture.pdf"},{"key":"e_1_2_1_2_97_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0263-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0263-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0263-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,16]],"date-time":"2025-04-16T21:58:38Z","timestamp":1744840718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0263-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":97,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["10.1007\/s00165-012-0263-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0263-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2014,3]]}}}