AN EXECUTABLE SPECIFICATION LANGUAGE FOR FAST PROTOTYPING PARALLEL RESPONSIVE SYSTEMS

摘要

An executable specification language, known as PSP, for fast prototyping parallel responsive systems is introduced. The language is equipped with directly executable mathematical data objects, first order predicates, temporal operators, parallel assignment, state and state history, sets, maps and sequences, etc. An abstract system model of a parallel responsive system may be constructed using PSP. Using this model, various dynamic behaviors of the system can be studied and analysed at an early design stage. These include detailed temporal relations between every component in the system. Temporal and functional properties of the system can also be expressed within PSP as (temporal) predicates. Global cause-effect relations and other temporal properties of the system can be tested by executing both the abstract system model and its associated functional/temporal assertions. Inconsistency and incompleteness in the abstract design can then be discovered against user's intention before real implementation, thus reducing design cost. PSP is illustrated using a lift system.