Formal Model for SDL Specifications Based on Timed Rewriting Logic

摘要

SDL (Specification and Description Language) is a standard industrial formal211u001edescription technique for real-time distributed systems which is based on 211u001ecommunicating finite state machines. Desptie its wide spread use and industrial 211u001eimportance SDL lacks at present a complete and integrated formal semantics. In 211u001ethis paper the authors begin to develop such a formal semantics for SDL using a 211u001enew algebra formalism called Timed Rewriting Logic (TRL). TRL is a specification 211u001eformalism which extends standard algebraic specification techniques by allowing 211u001ethe dynamic behavior of systems to be axiomatised using term rewriting rules. The 211u001erewrite rules can be labelled with time constraints which provide a means of 211u001ereasoning about time elapse in real-time systems. The formal semantics the 211u001eauthors develop catures in an intuitive way the hierarchical structure of SDL 211u001especifications and integrates within one formalism the static and dynamic aspects 211u001eof an SDL system. It also provides a natural basis for analyzing, verifying, 211u001etesting and composing SDL systems.