Proving Properties of Operation Contracts with Test Scenarios
This contribution studies structural and behavioral models by applying (a) UML classes, associations, attributes, generalization and OCL invariants for structural model features and (b) UML operations and OCL contracts, i.e., pre- and postconditions, for behavioral features. For detecting and assuring model properties that are not explicitly present, but valid in the considered model suitable test cases are constructed. Inspected model properties are: (a) the consistency between the invariants and the contracts, including the consistency between operation calls by checking whether the postcondition of one operation is compatible with the precondition of a following operation, and (b) the reachability of particular model states characterized by invariant-like OCL formulas through an operation call chain. Thus, by constructing test cases we prove model consistency and property reachability for operation calls.
Wed 19 JulDisplayed time zone: London change
11:15 - 12:45 | TAP Session 4: Model-based test generationResearch Papers at Willow Chair(s): Nico Naus Virginia Tech Remote Participants: Zoom Link | ||
11:15 30mTalk | Symbolic Observation Graph-Based Generation of Test Paths Research Papers P: Kais Klai Universit Paris 13, Mohamed Taha Bennani Universty of Tunis El Manar, Jaime Arias CNRS; LIPN; Université Sorbonne Paris Nord, Jörg Desel Fernuniversität in Hagen, Hanen Ochi EFREI DOI File Attached | ||
11:45 30mTalk | Testing Languages with a Languages-as-databases ApproachTAP Best Paper Research Papers DOI | ||
12:15 30mTalk | Proving Properties of Operation Contracts with Test Scenarios Research Papers DOI |