Specifying embedded systems with statecharts and Z: an agenda for cyclic software components

The application of formal techniques can contribute much to the quality of software, which is of utmost importance for safety-critical embedded system s. These techniques, however, are not easy to apply. In particular, methodo logical guidance is often unsatisfactory. We address this problem by the co ncept of an agenda, An agenda is a list of activities to be performed for s olving a task in software engineering. Agendas used to support the applicat ion of formal specification techniques provide detailed guidance for specif iers, templates of the used specification language that only need to be ins tantiated, and application independent validation criteria. We apply the ag enda approach to a particular class of embedded safety-critical systems, th e formal specification of which has been investigated in the case-studies o f the German project during the last two years. (C) 2001 Elsevier Science B .V. All rights reserved.