Safety-Guarantee Controller Synthesis for Cyber-Physical Systems

Details Safety-Guarantee Controller Synthesis for Cyber-Physical Systems Safety-Guarantee Controller Synthesis for Cyber-Physical Systems

2010-10-27

arxiv.org/abs/1010.5665v1

Computer Science

Logic in Computer Science

Scientific paper

The verification and validation of cyber-physical systems is known to be a difficult problem due to the different modeling abstractions used for control components and for software components. A recent trend to address this difficulty is to reduce the need for verification by adopting correct-by-design methodologies. According to the correct-by-design paradigm, one seeks to automatically synthesize a controller that can be refined into code and that enforces temporal specifications on the cyber-physical system. In this paper we consider an instance of this problem where the specifications are given by a fragment of Linear Temporal Logic (LTL) and the physical environment is described by a smooth differential equation. The contribution of this paper is to show that synthesis for cyber-physical systems is viable by considering a fragment of LTL that is expressive enough to describe interesting properties but simple enough to avoid Safra's construction. We report on two examples illustrating a preliminary implementation of these techniques on the tool PESSOALTL.

Affiliated with

Also associated with

No associations

Rating

Safety-Guarantee Controller Synthesis for Cyber-Physical Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Safety-Guarantee Controller Synthesis for Cyber-Physical Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Safety-Guarantee Controller Synthesis for Cyber-Physical Systems will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-485573