Dagstuhl Seminar 2009: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>WikiSysop |
imported>WikiSysop |
||
| (2 intermediate revisions by the same user not shown) | |||
| Line 3: | Line 3: | ||
[http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=09381 Dagstuhl Seminar Page] | [http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=09381 Dagstuhl Seminar Page] | ||
Members of the Deploy project participated in a | Members of the Deploy project participated in a Dagstuhl Seminar on ''Refinement Based Methods for the Construction of Dependable Systems'' from 13 to 18 September 2009. For more details see the [http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=09381 Dagstuhl seminar web page]. | ||
One of the outcomes of that seminar was the identification of a list of '''challenging issues faced by industrial users of formal methods'''. | One of the outcomes of that seminar was the identification of a list of '''challenging issues faced by industrial users of formal methods'''. | ||
| Line 19: | Line 19: | ||
* Proof automation | * Proof automation | ||
* Proof reuse | * Proof reuse | ||
* | * Handling complex data structures | ||
* | * Code generation | ||
* | * Test case generation | ||
* | * Handling assumptions about the environment | ||
Latest revision as of 13:31, 3 November 2009
Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems
Members of the Deploy project participated in a Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems from 13 to 18 September 2009. For more details see the Dagstuhl seminar web page.
One of the outcomes of that seminar was the identification of a list of challenging issues faced by industrial users of formal methods. The list may be of wider interest so is reproduced here:
- Team-based development
- Heavy model re-factoring
- Linking requirements engineering and FMs
- Abstraction is difficult
- Refinement strategies
- Guidelines for method and tool selection
- Keeping models and code in sync
- Real-time modelling
- Supporting reuse and variants
- Proof automation
- Proof reuse
- Handling complex data structures
- Code generation
- Test case generation
- Handling assumptions about the environment
