Jastram, Michael and Hallerstede, Stefan and Leuschel, Michael and Russo Jr, Aryldo G (2010) An Approach of Requirements Tracing in Formal Refinement. In: VSTTE’10 Verified Software: Theories, Tools and Experiments, 16th-19th August 2010, Edinburgh, UK. (In Press)
This is the latest version of this item.
![[img]](../style/images/fileicons/application_pdf.png)
| PDF - Accepted Version 562Kb |
Abstract
Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements. We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Uncontrolled Keywords: | Requirements Traceability, WRSPM, Formal Modeling, Refinement, Event-B |
| Subjects: | Methodology > Requirements and evolution Training > Rodin plug-ins |
| ID Code: | 236 |
| Deposited By: | Mr Michael Jastram |
| Deposited On: | 08 Jul 2010 10:48 |
| Last Modified: | 18 Jul 2010 23:51 |
Available Versions of this Item
- An Approach of Requirements Tracing in Formal Refinement. (deposited UNSPECIFIED)
- An Approach of Requirements Tracing in Formal Refinement. (deposited 08 Jul 2010 10:48) [Currently Displayed]
Repository Staff Only: item control page
