The Logic of Communicating Shared Resources

This page is under construction.
The use of temporal logics to express properties of specifications is well-established. Model checking is commonly used to verify that the property expressed as a logical formula holds for a given system specification.
A highly expressive real-time logic LCSR is proposed as means to express properties of ACSR specifications. The logic contains primitives allowing users to deal with resource usage and timing properties of a specification.

LCSR provides a flexible two-level language for property specification. On the user level, it represents properties graphically in terms of the user's domain.
The second level, oriented towards a formal methods expert, is used to define domain-specific user-level constructs. Each user-level construct is represented as a fragment of a logical formula. New constructs can be added dynamically as needed. The rules of the language guarantee the well-formedness of formulas.

The LCSR tool features a graphical editor for user-level specifications, and a verification engine that implements an efficient local model checking algorithm.

Publications