Seminars

Modeling and Verification of Real-Time/Hybrid/Cyber-Physical Systems via Concurrent Co-inductive Constraint Logic Programming PDF files
Neda Saeedloei - University of Texas at Dallas

05/24/2010, 3pm, GHC-6115

Abstract

Design, specification, implementation and verification of real-time systems is an important area of research as real-time systems are ubiquitous. Research in this area has resulted in formalisms for incorporation of time in computation, frameworks for specifying real-time systems and also verification tools and techniques for verifying interesting properties of such systems. Most efforts incorporate time by discretizing it. In this talk I will present the techniques that we have developed for including continuous time in computation. These techniques are general techniques that can be used not only for modeling continuous time but also various physical quantities such as temperature, pressure, etc. My work has focused on developing frameworks for specifying and verifying realtime/hybrid systems and cyber-physical systems. This framework is based on logic programming extended with constraints and co-induction. I will present our investigation on incorporation of continuous time in various domains of computer science. In particular the extension of grammars with continuous time (timed grammars) and also _-calculus with continuous time (timed _-calculus) will be presented.

Biography

Neda Saeedloei is a doctoral candidate in the department of computer science at University of Texas at Dallas. She received the B.S. degree in applied Mathematics from Sharif University of Technology in 1997 and the M.S. degree in computer science from University of Texas at Dallas in 2007. Her research interests are in modeling and verification of real-time systems/hybrid systems and cyber-physical systems, model checking, logic programming, constraint logic programming and co-inductive logic programming.