|
|
|
|
 |
|
|||||||||||||||||||
 |
Application name: B27 Traffic Control System Organisation: DST Deutsche System-Technik GmbH Method: Z Tools: DST-fuzz type checker Domain: Miscellaneous Period: 1994 - 1995 Size: approximately five people in the overall team; one person doing the formal specifications; approximately 120 pages of Z specification (at the time of report). Description: The system implemented in this project is designed to control the traffic flow on a piece of motor-way in southern Germany. The applications, which analyze traffic- and weather data and automatically or manually control traffic signs along the route according to this data, were identified to be critical for proper operation of the overall system. Therefore it was decided to produce a formal specification for these as a reference for later implementation. These pieces will be embedded into the structured specification for the rest of the system. Conclusions: No final conclusions possible at the time of report, since the project is still running. We heavily underestimated the effort needed to completely understand (and specify) the selected applications, since it turned out, that a lot of information was not available in the underlying requirements document and either had to be drawn from the applications expert's mind or from different documents. In a traditional implementation process, this underestimation surely would have lead to a drastic delay of the coding phase. It was encouraging how detailed the review of the specifications together with the customer was and that many open or misunderstood issues could be cleared up during these reviews. Publications: - Contact:
URL: Remarks: - |
|||||||||||||||||||
 |
||||||||||||||||||||
|
||||||||||||||||||||
© copyright 2004 | Formal Methods Europe |
||||||||||||||||||||
