Embedded Real-time/Hybrid Systems
In this effort we are interested in reliable construction of embedded
real-time/hybrid systems. The research includes developing
domain specific languages for reliably constructing
embedded real-time/hybrid systems, constraint based verification of
these systems, and automation of software-hardware design
decisions based on constraint solving. At present, we are developing
a provably correct compiler for the specification language of SCR (software
cost reduction), developed at the Naval Research Labs.
Papers
-
G. Gupta, E. Pontelli. "A Constraint-based Approach to
Specification and Verification of Real-time Systems,"
In Proc. IEEE Real-time Symposium, San Francisco, pp. 230-239.
Dec. '97.
-
L. King, G. Gupta, E. Pontelli.
Verification of BART Controller: An Approach based on Horn
Logic and Denotational Semantics. In High
Integrity Software Systems, Kluwer Academic, to appear.
-
G. Gupta and E. Pontelli. A Horn Logic Denotational Framework
for Specification, Implementation, and Verification of Domain
Specific Languages, To appear, 2001.