Projekt

Type Analysis for Component-based Real-time Programming (REALTYPE)

The overall aim of this project is to open up and explore a new route for transferring formal methods technology into software industry, by extending the conventional type-checking paradigm. Specifically, the aim is to develop an automatic validation method based on the notion of real-time process types in combination with rigorous semantic models that

permits the specification of static functional, reactive, and temporal requirements
combines and adapts standard type-checking, model-checking, and timing-analysis techniques
is specialised for use in component-based interactive programming environments in the signal processing and control area.

To achieve these aims the project investigates new semantic theories

for cycle-based programming under the synchrony hypothesis, which adress the notorious problems of compositionality and full-abstraction known from synchronous programming languages, such as Statecharts and Esterel
to obtain a compositional coordination model for capturing the globally synchronous and locally asynchronous scheduling of digital-signal-processing-and-control tools, specifically ICONNECT
in which emphasis is given to supporting hierarchical dataflow graphs and to the concept of run-to-completion and isochronic broadcast.

Projektleitung:
Prof. Michael Mendler, Ph.D., Gerald Lüttgen, The University of York, UK

Beteiligte:
Barry Norton, Universität Sheffield, Prof. Dr. Werner Grass, Universität Passau, Dr. Bernhard Sick, Universität Passau

Laufzeit: 1.5.2000 - 30.4.2003

Förderer:
British EPSRC
British Council
DAAD

Mitwirkende Institutionen:
Roland Mandl, Micro-Epsilon GmBH, Ortenburg

Publikationen

Norton, B. ; Luettgen, G. ; Mendler, Michael: A compositional semantic theory for synchronous component-based design . In: Amadio, R. ; Lugiez, D. (Hrsg.) : Int`l Conference on Concurrency Theory (Concur`03 Marseille Sept. 2003). Berlin u.a. : Springer, 2003, S. 461-476. (LNCS Bd. 2761)

Sicheneder, A. ; Bender, A. ; Fuchs, E. ; Mendler, Michael ; Sick, B.: Tool-supported software design and program execution for signal processing applications using modular software components . In: Margaria, T. ; Steffen, B. (Hrsg.) : Proceedings International Workshop on Software Tools for Technology Transfer (STTT'98 University of Aalborg, Denmark June 1998). 1998, S. 61-70.

Lüttgen, G. ; Mendler, Michael ; Maraninchi, F. (Hrsg.): Proc. Semantic Foundations of Engineering Design Languages (SFEDL'02) . (SFEDL'02 Grenoble April 2002) 2002. - 137 Seiten.

Lüttgen, G. (Hrsg.) ; Martinez Madrid, N. ; Mendler, M.: Proceedings Semantic Foundations of Engineering Design Languages (SFEDL'04) . München : Elsevier, 2004 (Electronic Notes in Theoretical Computer Science Bd. to appear) . - 90 Seiten.

Broy, M. ; Lüttgen, G. ; Mendler, Michael (Hrsg.): Special Issue: Semantic Foundations of Engineering Design Languages . London : Springer, 2004 (Journal of Formal Aspects of Computing Bd. to appear)

Norton, B.: Reactive Types for Dataflow-Oriented Component-Based Design . In: University of Birmingham (Veranst.) : 2nd Workshop in the Automated Verification of Critical Systems (AVoCS02). Birmingham : University of Birmingham, 2002, S. 195-209. (University of Birmingham Technical Report CRS-02-6)

Luettgen, G. ; Mendler, Michael: Fully-abstract statecharts semantics via intuitionistic Kripke models . In: Montanari, U. ; Rolim, J. ; Welzl, E. (Hrsg.) : 27th Int'l Colloquium on Automata, Languages and Programming (ICALP 2000). Berlin u.a. : Springer, 2000, S. 163-174. (LNCS Bd. 1853)

Luettgen, G. ; Mendler, Michael: The intuitionism behind statecharts steps . Hampton, V.A., USA : NASA Langley Research Center. 2000 (NASA, Institute for Computer Applications in Science and Engineering ICASE, Report CR-2000-210302). - Forschungsbericht. 40 Seiten

Lüttgen, G. ; Mendler, Michael: What is in a Step: A fully abstract semantics for Statecharts macro steps via intuitionistic Kripke models . Sheffield : University of Sheffield. 2000 (CS-00-04). - Interner Bericht. 48 Seiten

Luettgen, G ; Mendler, Michael: Statecharts: From visual syntax to model-theoretic semantics . In: Bauknecht, K. ; Brauer, W. ; Mueck, Th. (Hrsg.) : Wirtschaft und Wissenschaft in der Network Economy-Visionen und Wirklichkeit (Workshop on Integrating Diagrammatic and Formal Specification Techniques Vienna September 2001). Bd. 1. Wien : Austrian Computer Society, 2001, S. 615-621.

Luettgen, G. ; Mendler, Michael: Axiomatizing an algebra of step reactions for synchronous languages . In: Brim, L. ; Jancar, P. ; Ketinsky, M. ; Kucera, A. (Hrsg.) : Int`l Conference on Concurrency Theory (CONCUR 02 Brno August 2002). Berlin u.a. : Springer, 2002, S. 386-401. (LNCS Bd. 2421)

Luettgen, G. ; Mendler, Michael: The intuitionism behind statecharts steps . In: ACM Transactions on Computational Logic 3 (2002), Nr. 1, S. 1-41

Broy, M. ; Lüttgen, G. ; Mendler, Michael (Hrsg.): Where theory and practice meet . London : Springer, 2003 (special Issue of Formal Aspects of Computing Bd. 15, Nr. 4) . - 125 Seiten.

Luettgen, G. ; Mendler, Michael: Towards a Model Theory for Esterel . In: Maraninchi, F. ; Girault, A. ; Rutten, E. (Hrsg.) : Synchronous Languages and Applications (SLAP`02 Grenoble April 2002). Bd. 65. Tulane : Elsevier Science Publ., 2002, S. 15 Seiten. (Electronic Notes in Theoretical Computer Science)