Návrh časově kritických systémů I: specifikace a verifikace

specification, verification, real time, timeliness, event, stimulus, response, deadline, time constraint, timed automaton, computational tree logic

During a system design phase, it can be required the system must generate responses both in a correct form and on-time, i.e., in pre-defined time interval measured from the time a corresponding stimulus has arosen. Especially, following phases are important and must be done in order to design such systems in a correct way: specification, verification and realization reflecting previously verified specification. In the contribution, which is the first from series of four contributions dedicated to problems related with design of time-critical systems (real-time systems, RT systems), specification and verification phases are introduced and illustrated by means of simple examples.