Modelling and Analysis of Real Time Systems with Logic Programming and Constraints

Gourinath Banda

Research output: Book/ReportPh.D. thesisResearch

Abstract

Embedded systems are increasingly being deployed in a wide variety of applica- tions. Most, if not all, of these applications involve an electronic controller with discrete behaviour controlling a continuously evolving plant. Because of their hybrid behaviour (discrete and continuous) and reactive behaviour, the formal verification of embedded systems pose new challenges. Linear Hybrid Automata (LHA) is a language for specifying systems with linear hybrid behaviour. Abstract interpretation is a formal theory for approximating the semantics of programming languages. Model checking is a technique to verify the reactive behaviour of concur- rent systems. Computation Tree Logic (CTL) is a temporal property specification language. Logic programming is a general purpose programming language based on predicate logic.
In this dissertation, the LHA models are verified by encoding them as con- straint logic programs. The constraint logic program (CLP) encoding an LHA model is first specialised and then a concrete minimal model (or possibly an ab- stract minimal model) for the residual program is computed. The abstract minimal model is computed by applying the theory of abstract interpretation. The com- puted minimal model forms the basis for verifying the LHA model. We consider two techniques to verify the reactive properties specified as CTL formulas: (i) reachability analysis and (ii) model checking.
A systematic translation of LHA models into constraint logic programs is de- fined. This is mechanised by a compiler. To facilitate forward and backward reasoning, two different ways to model an LHA are defined. A framework consist- ing of general purpose constraint logic program tools is presented to accomplish the reachability analysis to verify a class of safety and liveness properties. A tool to compute the concrete minimal model is implemented. The model checking of CTL is defined as a concrete CTL-semantic function. Since model checking of infinite state systems, which LHAs are, does not terminate, we apply the theory of abstract interpretation to model checking that ensures termination at the cost of loss in precision. An abstract CTL-semantic function is constructed as an abstract interpretation of the CTL-semantic function. This abstract CTL-semantic func- tion is implemented using a SMT solver resulting in an abstract model checker. We consider two abstract domains: (i) the domain of constraints and (ii) the do- main of convex polyhedra, for both abstract model checking and abstract minimal model computation.
We demonstrate the applicability of the proposed theory with examples taken from the literature.
Original languageEnglish
PublisherRoskilde Universitet
Number of pages165
Publication statusPublished - Sep 2010
SeriesRoskilde Universitet. Computer Science. Computer Science Research Report
Number130
ISSN0109-9779

Cite this

Banda, G. (2010). Modelling and Analysis of Real Time Systems with Logic Programming and Constraints. Roskilde Universitet. Roskilde Universitet. Computer Science. Computer Science Research Report, No. 130
Banda, Gourinath. / Modelling and Analysis of Real Time Systems with Logic Programming and Constraints. Roskilde Universitet, 2010. 165 p. (Roskilde Universitet. Computer Science. Computer Science Research Report; No. 130).
@phdthesis{dc2c3e4acf184a199025d46fc5500720,
title = "Modelling and Analysis of Real Time Systems with Logic Programming and Constraints",
abstract = "Embedded systems are increasingly being deployed in a wide variety of applica- tions. Most, if not all, of these applications involve an electronic controller with discrete behaviour controlling a continuously evolving plant. Because of their hybrid behaviour (discrete and continuous) and reactive behaviour, the formal verification of embedded systems pose new challenges. Linear Hybrid Automata (LHA) is a language for specifying systems with linear hybrid behaviour. Abstract interpretation is a formal theory for approximating the semantics of programming languages. Model checking is a technique to verify the reactive behaviour of concur- rent systems. Computation Tree Logic (CTL) is a temporal property specification language. Logic programming is a general purpose programming language based on predicate logic.In this dissertation, the LHA models are verified by encoding them as con- straint logic programs. The constraint logic program (CLP) encoding an LHA model is first specialised and then a concrete minimal model (or possibly an ab- stract minimal model) for the residual program is computed. The abstract minimal model is computed by applying the theory of abstract interpretation. The com- puted minimal model forms the basis for verifying the LHA model. We consider two techniques to verify the reactive properties specified as CTL formulas: (i) reachability analysis and (ii) model checking.A systematic translation of LHA models into constraint logic programs is de- fined. This is mechanised by a compiler. To facilitate forward and backward reasoning, two different ways to model an LHA are defined. A framework consist- ing of general purpose constraint logic program tools is presented to accomplish the reachability analysis to verify a class of safety and liveness properties. A tool to compute the concrete minimal model is implemented. The model checking of CTL is defined as a concrete CTL-semantic function. Since model checking of infinite state systems, which LHAs are, does not terminate, we apply the theory of abstract interpretation to model checking that ensures termination at the cost of loss in precision. An abstract CTL-semantic function is constructed as an abstract interpretation of the CTL-semantic function. This abstract CTL-semantic func- tion is implemented using a SMT solver resulting in an abstract model checker. We consider two abstract domains: (i) the domain of constraints and (ii) the do- main of convex polyhedra, for both abstract model checking and abstract minimal model computation.We demonstrate the applicability of the proposed theory with examples taken from the literature.",
author = "Gourinath Banda",
year = "2010",
month = "9",
language = "English",
publisher = "Roskilde Universitet",

}

Banda, G 2010, Modelling and Analysis of Real Time Systems with Logic Programming and Constraints. Roskilde Universitet. Computer Science. Computer Science Research Report, no. 130, Roskilde Universitet.

Modelling and Analysis of Real Time Systems with Logic Programming and Constraints. / Banda, Gourinath.

Roskilde Universitet, 2010. 165 p. (Roskilde Universitet. Computer Science. Computer Science Research Report; No. 130).

Research output: Book/ReportPh.D. thesisResearch

TY - BOOK

T1 - Modelling and Analysis of Real Time Systems with Logic Programming and Constraints

AU - Banda, Gourinath

PY - 2010/9

Y1 - 2010/9

N2 - Embedded systems are increasingly being deployed in a wide variety of applica- tions. Most, if not all, of these applications involve an electronic controller with discrete behaviour controlling a continuously evolving plant. Because of their hybrid behaviour (discrete and continuous) and reactive behaviour, the formal verification of embedded systems pose new challenges. Linear Hybrid Automata (LHA) is a language for specifying systems with linear hybrid behaviour. Abstract interpretation is a formal theory for approximating the semantics of programming languages. Model checking is a technique to verify the reactive behaviour of concur- rent systems. Computation Tree Logic (CTL) is a temporal property specification language. Logic programming is a general purpose programming language based on predicate logic.In this dissertation, the LHA models are verified by encoding them as con- straint logic programs. The constraint logic program (CLP) encoding an LHA model is first specialised and then a concrete minimal model (or possibly an ab- stract minimal model) for the residual program is computed. The abstract minimal model is computed by applying the theory of abstract interpretation. The com- puted minimal model forms the basis for verifying the LHA model. We consider two techniques to verify the reactive properties specified as CTL formulas: (i) reachability analysis and (ii) model checking.A systematic translation of LHA models into constraint logic programs is de- fined. This is mechanised by a compiler. To facilitate forward and backward reasoning, two different ways to model an LHA are defined. A framework consist- ing of general purpose constraint logic program tools is presented to accomplish the reachability analysis to verify a class of safety and liveness properties. A tool to compute the concrete minimal model is implemented. The model checking of CTL is defined as a concrete CTL-semantic function. Since model checking of infinite state systems, which LHAs are, does not terminate, we apply the theory of abstract interpretation to model checking that ensures termination at the cost of loss in precision. An abstract CTL-semantic function is constructed as an abstract interpretation of the CTL-semantic function. This abstract CTL-semantic func- tion is implemented using a SMT solver resulting in an abstract model checker. We consider two abstract domains: (i) the domain of constraints and (ii) the do- main of convex polyhedra, for both abstract model checking and abstract minimal model computation.We demonstrate the applicability of the proposed theory with examples taken from the literature.

AB - Embedded systems are increasingly being deployed in a wide variety of applica- tions. Most, if not all, of these applications involve an electronic controller with discrete behaviour controlling a continuously evolving plant. Because of their hybrid behaviour (discrete and continuous) and reactive behaviour, the formal verification of embedded systems pose new challenges. Linear Hybrid Automata (LHA) is a language for specifying systems with linear hybrid behaviour. Abstract interpretation is a formal theory for approximating the semantics of programming languages. Model checking is a technique to verify the reactive behaviour of concur- rent systems. Computation Tree Logic (CTL) is a temporal property specification language. Logic programming is a general purpose programming language based on predicate logic.In this dissertation, the LHA models are verified by encoding them as con- straint logic programs. The constraint logic program (CLP) encoding an LHA model is first specialised and then a concrete minimal model (or possibly an ab- stract minimal model) for the residual program is computed. The abstract minimal model is computed by applying the theory of abstract interpretation. The com- puted minimal model forms the basis for verifying the LHA model. We consider two techniques to verify the reactive properties specified as CTL formulas: (i) reachability analysis and (ii) model checking.A systematic translation of LHA models into constraint logic programs is de- fined. This is mechanised by a compiler. To facilitate forward and backward reasoning, two different ways to model an LHA are defined. A framework consist- ing of general purpose constraint logic program tools is presented to accomplish the reachability analysis to verify a class of safety and liveness properties. A tool to compute the concrete minimal model is implemented. The model checking of CTL is defined as a concrete CTL-semantic function. Since model checking of infinite state systems, which LHAs are, does not terminate, we apply the theory of abstract interpretation to model checking that ensures termination at the cost of loss in precision. An abstract CTL-semantic function is constructed as an abstract interpretation of the CTL-semantic function. This abstract CTL-semantic func- tion is implemented using a SMT solver resulting in an abstract model checker. We consider two abstract domains: (i) the domain of constraints and (ii) the do- main of convex polyhedra, for both abstract model checking and abstract minimal model computation.We demonstrate the applicability of the proposed theory with examples taken from the literature.

M3 - Ph.D. thesis

BT - Modelling and Analysis of Real Time Systems with Logic Programming and Constraints

PB - Roskilde Universitet

ER -

Banda G. Modelling and Analysis of Real Time Systems with Logic Programming and Constraints. Roskilde Universitet, 2010. 165 p. (Roskilde Universitet. Computer Science. Computer Science Research Report; No. 130).