guest ::
| Home > Academic theses (ETDs) > Doctoral theses > Formal Verfication of Components in Java |
Original title:
Formal Verfication of Components in Java
Translated title: Formal Verfication of Components in Java
Authors: Parízek, Pavel ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Pasareanu, Corina (referee)
Document type: Doctoral theses
Year: 2008
Language: eng
Abstract: Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/17680
Permalink: http://www.nusl.cz/ntk/nusl-294410
The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Doctoral theses
Translated title: Formal Verfication of Components in Java
Authors: Parízek, Pavel ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Pasareanu, Corina (referee)
Document type: Doctoral theses
Year: 2008
Language: eng
Abstract: Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/17680
Permalink: http://www.nusl.cz/ntk/nusl-294410
The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Doctoral theses
Record created 2017-04-25, last modified 2022-03-04