Eingang zum Volltext in OPUS

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:kobv:83-opus-30900
URL: http://opus.kobv.de/tuberlin/volltexte/2011/3090/

Krieger, Matthias P. ; Knapp, Alexander

Executing Underspecified OCL Operation Contracts with a SAT Solver

pdf-Format:
Dokument 1.pdf (262 KB)
Print-on-Demand:

Kurzfassung auf Englisch

Executing formal operation contracts is an important technique for requirements
validation and rapid prototyping. Current approaches require additional
guidance from the user or exhibit poor performance for underspecified contracts
that describe the operation results non-constructively. We present an efficient and fully automatic approach to executing OCL operation contracts which uses a satisfiability (SAT) solver. The operation contract is translated to an arithmetic formula with bounded quantifiers and later to a satisfiability problem. Based on the system state in which the operation is called and the arguments to the operation, an off-the-shelf SAT solver computes a new state that satisfies the postconditions of the operation. An effort is made to keep the changes to the system state as small as possible.
We present a tool for generating Java method bodies for operations specified
with OCL. The efficiency of our method is confirmed by a comparison with existing approaches.

Freie Schlagwörter (Deutsch): OCL, Model execution, Animation, SAT solvers
Freie Schlagwörter (Englisch): OCL, Model execution, Animation, SAT solvers
Collection: TU Berlin / Zeitschriften / Fakultät IV - Elektrotechnik und Informatik / Electronic Communications of the EASST- ECEASST / Volume 15 (2008): OCL Concepts and Tools 2008
Institut: Institut für Softwaretechnik und Theoretische Informatik
DDC-Sachgruppe: Informatik
Dokumentart: Aufsatz
Schriftenreihe: Electronic Communications of the EASST- ECEASST
Bandnummer: 15/06
ISBN/ISSN: 1863-2122
Quelle: http://journal.ub.tu-berlin.de/eceasst/article/view/176/
Sprache: Englisch
Erstellungsjahr: 2008
Publikationsdatum: 21.06.2011
Lizenz: Standardlizenz: Typ CC by-nc-sa - Namensnennung erforderlich | Kommerziell nein | Weiterbearbeitung nur unter gleichen Bedingungen erlaubt | PoD ja