Original title:
Extending Java PathFinder with Behavior Protocols
Translated title:
Extending Java PathFinder with Behavior Protocols
Authors:
Plšek, Aleš ; Kofroň, Jan (referee) ; Adámek, Jiří (advisor) Document type: Master’s theses
Year:
2006
Language:
eng Abstract:
[eng][cze] The Component-based programming is an aproach to efficient development of software applications, where Behavior protocol is a formalism used for behavior specification of components. To further ease the development of a component application, System Correctness analysis is employed to discover errors at the designe time. However, without verifying that a component implementation complies with its behavior protocol, the analysis of the system could be based on unsatisfied property. This thesis addresses the problem of verification that a component implementation adheres to its behavior protocol. By employing Java PathFinder Model Checker it offers an ambitious solution which is successfully addressing one of the issues of the software component development.Komponentově orientované programování, vyuřívající behavior protokoly pro specifikaci chovaní komponent, představuje efektivní přístup k vývoji softwarových aplikací. Jedním z prostředků jak ještě více usnadnit vývoj je i analýza korektnosti systému. Avšak bez ověření, že implementace komponent dodržují dané behavior protokoly, nemůže být analýza korektnosti systému formálně považována za úplnou. Tato práce předkládá způsob jak ověřit, zda je implementace komponenty v souladu s daným behavior protokolem. Navržené řešení využívá nástroj Java PathFinder Model Checker k ověření implementace komponenty a tímto ambiciózním způsobem úspěšně čelí jednomu z otevřených problémů při vývoji komponentových aplikací.
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/7122