Neil Evans has been visiting the School from Royal Holloway, University of London and will give a seminar tomorrow based on a paper he is presenting to SEFM in Beijing next week.
EB3 is an established formal technique, based on process algebra, for specifying Information Systems (IS) that have both complex state and event based features; as yet, EB3 has no tool support. Another formal technique called CSP || B uses two existing analysis tools, FDR and the B-Toolkit, to support the verification of state/event based systems. However, the CSP || B approach has never been applied to this specialised domain. In this paper, we use a specification pattern of EB3 to motivate a new style of specification in CSP || B appropriate for IS. We demonstrate this using an example system and show that the verification of its dynamic properties is now amenable to tool support.
| Neil Evans |
| Royal Holloway, University of London |
| Date: | Thu Sep 23 2004 |
| Time: | 3:00 to 3:45pm |
| Location: | Level 2 Seminar Room (201B), CSE Bldg (K17), UNSW Kensington campus |
Last updated by tbourke at Thu Sep 23 12:15:13 2004 GMT+1000