Keywords: Discrete Event Systems, System Engineering, Autonomous Decentralized Systems
Abstract: Organizer: Masaki Nakamura (Toyama Prefectural University)
Co-organizer: Kazutoshi Sakakibara (Toyama Prefectural
University)
Statement of Objectives:
To provide a clear introduction to the OTS/CafeOBJ method
for modeling and verifying multitask real-time systems. In
this approach, systems are modeled as observational
transition systems (OTSs), and their specifications are
written in CafeOBJ, an algebraic specification language.
Participants will learn how to describe system behavior and
time constraints using the CafeOBJ language/system, and how
to verify safety properties using the proof score method
through concrete examples.
Intended Audience:
This tutorial is intended for researchers, engineers, and
students who are interested in formal methods for
concurrent and real-time systems. No prior experience with
CafeOBJ is required, although basic knowledge of
mathematics, logic, and programming is helpful. In this
tutorial, we first introduce the basic ideas of the
OTS/CafeOBJ method, and then explain how to model and
describe time constraints in OTS/CafeOBJ specifications
through a small example. Then, as case studies, we present
Fischer’s mutual exclusion protocol and an autonomous
vehicle group control system.
The duration of the tutorial can be adjusted from 60
minutes to a half day (180 minutes).
List of Speakers: Masaki Nakamura (Toyama Prefectural
University)
List of Topics: CafeOBJ, Observational transition system,
Formal methods, Real-time Hybrid system