Techniques for Reactive System Design: The Tools in TRADE

Abstract. Reactive systems are systems whose purpose is to maintain a certain desirable state of affairs in their environment, and include infor-mation systems, groupware, workflow systems, and control software. The current generation of information system design methods cannot cope with the high demands that originate from mission-critical application, geographic distribution, and a mix of data-intensive, behavior-intensive and communication-intensive properties of many modern reactive sys-tems. We define an approach to designing reactive software systems that deals with these dimensions by incorporating elements from various in-formation system and software design techniques and extending this with formal specification techniques, in particular with model checking. We illustrate our approach with a smart card application and show how in-formal techniques can be combined with model checking.