About: Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1, which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking. Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1, which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking. (en)
Title	Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker (en)
skos:prefLabel	Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker (en)
skos:notation	RIV/00216208:11320/07:10084051!RIV11-GA0-11320___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(GA201/06/0770), Z(AV0Z10300504), Z(MSM0021620838)
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Kofroň, Jan Parízek, Pavel Plášil, František
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Univerzita Karlova v Praze / Matematicko-fyzikální fakulta
http://linked.open...dnocenehoVysledku	434195
http://linked.open...ai/riv/idVysledku	RIV/00216208:11320/07:10084051
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	model checking; behavior protocols; software components (en)
http://linked.open.../riv/klicoveSlovo	model checking software components behavior protocols
http://linked.open...ontrolniKodProRIV	[4BA19DFA97C0]
http://linked.open...v/mistoKonaniAkce	Loyola College, Columbia, MD, USA
http://linked.open...i/riv/mistoVydani	Neuveden
http://linked.open...i/riv/nazevZdroje	30th IEEE/NASA Software Engineering Workshop (SEW-30)
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Formal methods applicable to development of component-based systems
http://linked.open...UplatneniVysledku	2007
http://linked.open...iv/tvurceVysledku	Kofroň, Jan Parízek, Pavel Plášil, František
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2006-04-25 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Informatika pro informační společnost: modely, algoritmy, aplikace Moderní metody, struktury a systémy informatiky
number of pages	8 (xsd:int)
http://purl.org/ne...btex#hasPublisher	IEEE Computer Society
https://schema.org/isbn	0-7695-2624-1
http://localhost/t...ganizacniJednotka	11320
is http://linked.open...avai/riv/vysledek of	Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 91 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software