Specification formalisms for real-time systems and advanced methods for analysis of formal specifications are important aspects of modern real-time systems development. Formal analysis helps the developers to find design problems early in the development cycle and gain confidence in the correctness of the system.
Algebra of Communicating Shared Resources (ACSR) is a real-time process algebra for specification of resource-bound real-time systems. VERSA analysis tool has been developed for verification of ACSR specifications.
Visual specification language Graphical Communicating Shared Resources (GCSR) is supported by the graphical PARAGON toolset.
LCSR is a real-time temporal logic with the ability to express the properties of resource usage.
Process algebra ACSR-VP extends ACSR with value passing. ACSR-VP is endowed with symbolic semantics, and algorithms for symbolic analysis of ACSR-VP specifications are developed.
A set of analysis methods for probabilistic systems is developed and applied to a probabilistic extension of ACSR.
A set of analysis methods for power-constrained, timed systems is developed and applied to an extension of ACSR that allows the modeling of probabilistic resource failures, priorities of resource usages, and power consumption by resourses within the same formalism.
Communicating Timed State Machines, CTSM, is a formal model for describing real-time systems. In CTSM, a system consists of concurrent processes communicating with each other through channels. Each process has data variables with arbitrary domain and clock variables with dense domain, where clock variables are special variables used to express various timing constraints such as delays and deadlines. CTSMs are compositional; that is, a CTSM process can be constructed by composing two CTSM processes.
TREAT is a verification tool for manipulation of CTSM.