Abstract
As domain modelling has been identified as a key issue for putting formal specification techniques into engineering practice, two reference case studies were elaborated within the research programme “Integration of Software Specification Techniques for Applications in Engineering”. One of them, coming from the railway transportation control domain and using an example of a radio based level crossing control system, was developed at the Institute of Traffic Safety and Automation Engineering. A physical railway model demonstrator was designed and developed as a means of comparison and validation for the formal specifications coming from partners involved in the research program.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arabestani, S., Bitsch, F., Gayen, J.-T.: Precise Definition of the Single-track Level Crossing in Radio-based Operation in UML Notation and Specification of Safety Requirements. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 119–144. Springer, Heidelberg (2004)
Abrial, J.-R., Börger, E., Langmaack, H. (eds.): Dagstuhl Seminar 1995. LNCS, vol. 1165. Springer, Heidelberg (1996)
Brill, M., Buschermöhle, R., Damm, W., Klose, J., Westphal, B., Wittke, H.: Formal Verification of LSCs in the Development Process. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 494–516. Springer, Heidelberg (2004)
Berkenköter, S., Bisanz, S., Hannemann, U., Peleska, J.: Hybrid UML and its Application to Specification and Test of Train Control Systems. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 145–173. Springer, Heidelberg (2004)
Bjørner, D., Braad, J., Mogensen, K.S.: Models of Railway Systems: Domain. Technical report, Dept. of IT, Techn. Univ. of Denmark (1999), Electronic version available http://www.ifad.dk/Projects/FMERail/proceedings3.htm
Bjørner, D.: Domain engineering: a precursor for requirements engineering and software design. Technical report, Dept. of Information Technology, Techn. Univ. of Denmark (1997–1998)
Bock, U.: Betriebs- und Kommunikationskonzept für dynamische Rendevous- Manöver von Zügen. Dissertation, Braunschweig. In: J.-Uwe Varchim [Hrsg.]. Berichte aus dem Institut für Elektrische Meßtechnik und Grundlagen der Elektrorechnik, Band 13 (2001) ISBN 3980818101
Einer, S.: STOP - Specification Technique of Operational Processes. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 227–247. Springer, Heidelberg (2004)
A product of Extessy AG, Germany
Betriebliches Lastenheft für FunkFahrBetrieb. Stand 1.10 (1996)
Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: A benchmark for comparing different approaches for specifying and verifying real-time systems. In: Procceedings Tenth International Workshop on Real-Time Operating Systems and Software (May 1993)
Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.: STATEMATE: A Working Environment for the Development of Complex. IEEE Transactions on Software Engineering 16, 403–414 (1990)
Krone, M.: Visual Formal Specification in Railway System Development. In: Doctoral Consortium of ISRE 1997, Annapolis, USA (1997)
MATLAB/Simulink r_ Product of The MathWorks, Inc.
Nilsson, T.: Application Domain Languages: Some Suggestions for Research. In: Gyimóthy, T. (ed.) CC 1996. LNCS, vol. 1060, pp. 1–4. Springer, Heidelberg (1996)
Ortner, E., Schienmann, B.: Normative language approach – a framework for understanding. In: Thalheim, B. (ed.) 15th Intern. Conf. on Conceptual modeling, pp. 261–276. Springer, Berlin (1996)
Ortmeier, F., Thums, A., Schellhorn, G., Reif, W.: Combining Formal Methods and Safety Analysis - The ForMoSA Approach. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 474–493. Springer, Heidelberg (2004)
Pachl, J.: Systemtechnik des Schienenverkehrs. Verlag B. G. Teubner, Stuttgart, Leipzig (1999)
Parthasarathy, S., Schnieder, E.: The explication problem: Achille’s heel of formal methods. In: 6. Fachtagung Entwicklung und Betrieb komplexer Automatisierungssysteme (EKA 1999), 1st edn., May 1999, pp. 93–103 (1999)
Schrom, H., Schnieder, E.: SCAN - A hardware minimised low cost / low power bus - A functional overview. In: MICRO.tec 2000, Hannover, February 2000, vol. 1, pp. 183–186 (2000), 25.-27.09.2000, Expo 2000
Schnieder, E., Jansen, L.: Traffic Control Systems Case Study: Problem. Description and Note on Domain-based Software Specification, Integration of Specification Techniques with Applications in Engineering. In: Forschungsbericht des Fachbereichs Informatik der TU Berlin (2000)
Snelting, G.: Paul Feyerabend und die Softwaretechnologie, Informatik Spektrum, Oktober 1998, pp. 273–276 (1998)
StP: Software through pictures, Product of AONIX
Lexique général des termes ferroviaires – Français, Deutsch, English, Italiano, Español, Nederlands. Union Internationale des Chemins de fer, Paris, 4th edn. (1988)
Thums, A., Schellhorn, G., Ortmeier, F., Reif, W.: Interactive Verification of Statecharts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 355–373. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hänsel, F., Poliak, J., Slovák, R., Schnieder, E. (2004). Reference Case Study “Traffic Control Systems” for Comparison and Validation of Formal Specifications Using a Railway Model Demonstrator. In: Ehrig, H., et al. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, vol 3147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27863-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-27863-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23135-6
Online ISBN: 978-3-540-27863-4
eBook Packages: Springer Book Archive