Fundamentals of Computing

Classifications: Software The research involves developing a theory of real-time process types for the static validation of signal processing and control applications. It will combine the standard methods of type checking, model-checking and timing analysis within one coherent analysis framework. The type-theory and its semantics will be based on a novel notion of clocked transition systems. Using semantic abstractions, several specialised type-checking algorithms for this type system will be developed corresponding to traditional type checking, model checking, and timing analysis. Semantic coherence will be ensured by systematically maintaining and solving abstraction constraints. The semantic foundation of clocked transition systems and the concept of abstraction and constraints in type theory builds on substantial recent research carried out by the investigator. The algorithms will be integrated into an existing programming tool, provided by the collaborators, and a case study to demonstrate the usefulness and efficiency of the algorithms will be undertaken. We expect that by extending the conventional type-checking paradigm as proposed the project will open up and explore a new route for transferring formal methods technology into software industry. The methods will support practical programming tools in the targeted domain to meet the high demands on correctness, real-time performance, and numeric precision