×

Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application. (English) Zbl 1342.93065


MSC:

93C15 Control/observation systems governed by ordinary differential equations
93A30 Mathematical modelling of systems (MSC2010)

Software:

Z; PVS; HOL; ML; HOL Light; Rodin
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, Cambridge · Zbl 0915.68015 · doi:10.1017/CBO9780511624162
[2] Abrial J-R (2010) Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge · Zbl 1213.68214 · doi:10.1017/CBO9781139195881
[3] 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-229 · Zbl 0807.68065
[4] Alur R., Dill D (1994) A theory of timed automata. Theor Comput Sci 126: 183-235 · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[5] Alur R., Henzinger T (1993) Real-time logics: complexity and expressiveness. Inf Comput 104: 35-77 · Zbl 0791.68103 · doi:10.1006/inco.1993.1025
[6] Alur R, Henzinger T (1994) A really temporal logic. J ACM 41: 181-204 · Zbl 0807.68065 · doi:10.1145/174644.174651
[7] Ahmed N (2006) Dynamic systems and control with applications. World Scientific, Singapore · Zbl 1127.93001 · doi:10.1142/6262
[8] Antsaklis P, Michel A (2006) Linear systems. Birkhauser, Boston · Zbl 1189.93001
[9] Banach R Model based refinement and the design of retrenchments. Available from [RET]
[10] 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-274
[11] Barnett S (1975) Introduction to mathematical control theory. Oxford University Press, Oxford · Zbl 0307.93001
[12] Bowen J, Hinchey M (1995) Seven more myths of formal methods. IEEE Softw 12: 34-41 · doi:10.1109/52.391826
[13] Bowen J, Hinchey M (1999) High-integrity system specification and design. Springer, Berlin · Zbl 0941.68029 · doi:10.1007/978-1-4471-3431-2
[14] Bowen J, Hinchey M (1999) Industrial-strength formal methods in practice. Springer, Berlin
[15] Banach R, Jeske C Retrenchment and refinement interworking: the tower theorems. Available from [RET] (Submitted) · Zbl 1361.68056
[16] Banach R, Jeske C, Poppleton M (2008) Composition mechanisms for retrenchment. J Log Algebraic Program 75: 209-229 · Zbl 1137.68037 · doi:10.1016/j.jlap.2007.11.001
[17] Börger E (2003) The ASM refinement method. FACJ 15: 237-257 · Zbl 1093.68601
[18] Banach R, Poppleton M, Jeske C, Stepney S (2007) Engineering and Theoretical Underpinnings of Retrenchment. Sci Comput Program 67: 301-329 · Zbl 1119.68348 · doi:10.1016/j.scico.2007.04.002
[19] Broenink J (2010) Embedded control software design with formal methods and engineering models. In: BCS-FACS Evening Seminar, September 2010 · Zbl 1171.68021
[20] Börger E, Stärk RF (2003) Abstract state machines. A method for high level system design and analysis. Springer, Berlin · Zbl 1040.68042 · doi:10.1007/978-3-642-18216-7
[21] Butler M Private communication
[22] Butler R (1996) NASA Technical Memorandum 110255. An introduction to requirements capture using PVS: specification of a simple autopilot. Technical report
[23] 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-78
[24] Banach R, Zhu H, Su W, Wu X Moded operation, continuous ASM, and an approach to pacemaker sensing (Submitted)
[25] Cau A, Moszkowski B, Zedan H Interval temporal logic. http://www.cse.dmu.ac.uk/ cau/papers/itlhomepage.pdf
[26] Chicone C (2006) Ordinary differential equations with applications. Springer, Berlin · Zbl 1120.34001
[27] Clarke F (1987) Optimization and nonsmooth analysis. Soc Ind Math · Zbl 0727.90045
[28] Clarke F, Ledyaev Y, Stern R, Wolenski P (1997) Nonsmooth analysis and control theory. Springer, Berlin · Zbl 1047.49500
[29] Crow, J.; Owre, S.; Rushby, J.; Shankar, N.; Srivas, M.; Larrondo-Petrie, M. (ed.); France, R. (ed.); Gerhart, S. (ed.), A tutorial introduction to PVS (1995), New York
[30] 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
[31] Derrick J, Boiten E (2001) Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, UK · Zbl 0982.68086 · doi:10.1007/978-1-4471-0257-1
[32] Dorf R, Bishop R (2010) Modern control systems. Pearson, Upper Saddle River · Zbl 0907.93001
[33] D’Azzo J, Houpis C (1995) Linear control system analysis and design: conventional and modern. McGraw Hill, New York · Zbl 0366.93001
[34] 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-161 · Zbl 1175.68243
[35] 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
[36] Debnath L, Mikusinski P (2005) Introduction to Hilbert Spaces with Applications. Springer, Berlin · Zbl 0715.46009
[37] de Roever WP, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. Cambridge University Press, Cambridge · Zbl 0955.68076 · doi:10.1017/CBO9780511663079
[38] Dutton K, Thompson S, Barraclough B (1997) The art of control engineering. Addison Wesley, New York
[39] Eshuis R (2009) Reconciling statechart semantics. Sci Comput Program, 74: 65-99 · Zbl 1171.68021 · doi:10.1016/j.scico.2008.09.001
[40] Franklin G, Powell J, Workman M (1996) Digital control systems. Prentice Hall, Upper Saddle River · Zbl 0697.93002
[41] Fadali M, Visioli A (2009) Digital control engineering: analysis and design. Academic Press, New York
[42] Gordon M, Melham T (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge · Zbl 0779.68007
[43] Hall J (1990) Seven myths of formal methods. IEEE Softw 5: 11-19 · doi:10.1109/52.57887
[44] Hall J (2007) Realising the benefits of formal methods. JUCS 13: 669-678
[45] Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer aided design. LNCS, vol 1166. Springer, Berlin
[46] 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łystok, pp 151-165 · Zbl 0743.68097
[47] 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-189
[48] Heitmeyer C (2007) Formal methods for specifying, validating, and verifying requirements. JUCS 13: 607-618
[49] Henzinger T (1996) The theory of hybrid automata. In: Proceedings of the IEEE LICS-96. IEEE, New York, pp 278-292.http://mtc.epfl.ch/ tah/Publications/the_theory_of_hybrid_automata.pdf · Zbl 0959.68073
[50] Horn R, Johnson C (1985) Matrix analysis. Cambridge University Press, Cambridge · Zbl 0576.15001 · doi:10.1017/CBO9780511810817
[51] Horn R, Johnson C (1991) Topics in matrix analysis. Cambridge University Press, Cambridge · Zbl 0729.15001 · doi:10.1017/CBO9780511840371
[52] Henzinger T, Kupferman O (1997) From quantity to quality. In: Proceedings of HART-97. LNCS, vol 1201. Springer, Berlin, pp 48-62
[53] Henzinger T, Manna Z, Pnueli A (1992) What good are digital clocks? In: Proceedings of ICALP-92. LNCS, vol 623. Springer, Berlin, pp 545-558 · Zbl 1425.68255
[54] Harrison J, Théry L (1998) A Skeptic’s approach to combining HOL and maple. J Autom Reason 21: 279-294 · Zbl 0916.68142 · doi:10.1023/A:1006023127567
[55] 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 · Zbl 1093.68601
[56] Jeske C (2005) Algebraic integration of retrenchment and refinement. PhD thesis, University of Manchester
[57] Kalman R (2005) Opening lecture, IFAC World Congress, Prague, Czech Republic, July 4 2005 · Zbl 1119.68348
[58] Karlsruhe Interactive Verifier. http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/
[59] Koymans R (1992) Specifying message passing and time-critical systems with temporal logic. LNCS, vol 651. Springer, Berlin · Zbl 0806.68074
[60] Kuo B (1992) Digital control systems. Oxford University Press, Oxford
[61] Lang S (1993) Real and functional analysis. Springer, Berlin · Zbl 0831.46001 · doi:10.1007/978-1-4612-0897-6
[62] Lester D (2007) Topology in PVS: continuous mathematics with applications. In: Rushby J, Shankar N (eds) Proceedings of AFM-07. ACM, New York
[63] Letier E (2001) Reasoning about agents in goal-oriented requirements engineering. PhD thesis, Dépt. Ingénierie Informatique, Université Catholique de Louvain
[64] 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-56 [See also: Technical Report CMU-CS-11-107 Carnegie Mellon University (2011)] · Zbl 1217.68066
[65] MacCluer B (2009) Elementary functional analysis. Springer, Berlin · Zbl 1170.46002 · doi:10.1007/978-0-387-85529-5
[66] Maple.http://www.maplesoft.com.m. Accessed 21 Sep 2012
[67] Mathematica.http://www.wolfram.com.m. Accessed 21 Sep 2012
[68] Meynadier J-M Private communication
[69] Matoussi A, Gervais F, Laleau R (2008) A first attempt to express kaos refinement patterns with event-B. In: Börger E, Butler M, Bowen JP, Boca P (eds) Proceedings ABZ-08. LNCS, vol 5238. Springer, Berlin · Zbl 1080.68058
[70] Olderog E-R, Dierks H (2008) Real-time systems: formal specification and automatic verification. Cambridge University Press, Cambridge · Zbl 1161.68030 · doi:10.1017/CBO9780511619953
[71] Ogata K (2008) Modern control engineering. Pearson, Upper Saddle River
[72] Ouaknine J (2002) Digitsation and Full Abstraction for Dense-Time Model Checking. In: Proceedings of TACAS-02, LNCS. Springer, Berlin, pp 37-51 · Zbl 1043.68581
[73] Paraskevopoulos P (1996) Digital control systems. Prentice Hall, Upper Saddle River · Zbl 0892.93003
[74] Platzer A (2010) Differential-algebraic dynamic logic for differential-algebraic programs. J Log Comput 20: 309-352 · Zbl 1191.03024 · doi:10.1093/logcom/exn070
[75] Platzer A (2010) Logical analysis of hybrid systems: proving theorems for complex dynamics. Springer, Berlin · Zbl 1211.68412 · doi:10.1007/978-3-642-14509-4
[76] 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-483 · Zbl 1287.03075
[77] Potter B, Sinclair J, Till D (1996) An introduction to formal specification and Z. Prentice Hall, Upper Saddle River · Zbl 0860.68069
[78] PVS Homepage.http://pvs.csl.sri.com.m. Accessed 21 Sep 2012
[79] Pytlak R (1999) Numerical methods for optimal control problems with state constraints. Lecture Notes in Mathematics, vol 1707. Springer, Berlin · Zbl 0928.49002
[80] Real J, Crespo A (2004) Mode change protocols for real-time systems: a survey and a new proposal. Real-Time Syst 26: 161-197 · Zbl 1069.68532 · doi:10.1023/B:TIME.0000016129.97430.c6
[81] Retrenchment Homepage.http://www.cs.man.ac.uk/retrenchment.t. Accessed 21 Sep 2012
[82] Rynne B, Youngson M (2000) Linear functional analysis. Springer, Berlin · Zbl 0945.46001 · doi:10.1007/978-1-4471-3655-2
[83] 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-455
[84] Schellhorn G (2001) Verification of ASM refinements using generalized forward simulation. JUCS 7: 952-979
[85] Schellhorn G (2005) ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor Comput Sci 336: 403-435 · Zbl 1080.68058 · doi:10.1016/j.tcs.2004.11.013
[86] Sontag E (1998) Mathematical control theory. Springer, Berlin · Zbl 0945.93001 · doi:10.1007/978-1-4612-0577-7
[87] Sekerinski E, Sere K (1998) Program development by refinement: case studies using the B-Method. Springer, Berlin · Zbl 0930.68087
[88] Stauner T (2002) Discrete-time refinement of hybrid automata. In: Proceedings of HSCC-02. LNCS, vol 2289. Springer, Berlin, pp 144-161 · Zbl 1044.93522
[89] Slissenko A, Vasilyev P (2008) Simulation of timed abstract state machines with predicate logic model checking. JUCS 14: 1984-2006 · Zbl 1217.68066
[90] 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-421
[91] 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]
[92] Tabuada P (2009) Verification and control of hybrid systems: a symbolic approach. Springer, Berlin · Zbl 1195.93001 · doi:10.1007/978-1-4419-0224-5
[93] van Lamsweerde A (2009) Requirements engineering: from system goals to uml models to software specifications. Wiley, New York
[94] Walter W (1998) Ordinary differential equations. Springer, Berlin · Zbl 0991.34001 · doi:10.1007/978-1-4612-0601-9
[95] Woodcock J, Davies J (1996) Using Z, specification, refinement and proof. Prentice Hall, Upper Saddle River · Zbl 0855.68060
[96] Willems J (2007) Open dynamical systems: their aims and their origins. Ruberti Lecture, Rome. http://homes.esat.kuleuven.be/ jwillems/Lectures/2007/Rubertilecture.pdf
[97] Zhou C, Hoare T, Ravn A (1991) A calculus of durations. Inf Proc Lett 40: 269-276 · Zbl 0743.68097 · doi:10.1016/0020-0190(91)90122-X
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.