Research On Verification Of Behaviors For SIGNAL Designed Multi-clock Embedded System

Nowadays,embedded systems are widely used in safety-critical areas such as aerospace,transportation,and nuclear energy.Software safety plays a more important role in people's lives and property.In the meantime,the system efficiency,resource utilization,response time,more than the clock properties and safety related properties become higher requirements in such system..How to design,validate and implement such system,is becoming a hot spot of academia and industry research problem.Embedded systems are sometimes composed of several components or subsystems,where each components based on different clock domains are integrated at system level.SIGNAL language is a convenient modeling method to express the multi-clock system.But it is not easy to verify the behavior of such system.Formal verification can provide rigorous mathematics proof for software models.This thesis is based on the formal method,and gives an efficient approach to verify the behavior of SIGNAL designed multi-clock embedded system in the system design phase.On the one hand,we proposes an approach to simulate the dataflow behaviors.On the other hand,we detect the boundedness problem.In order to find the potential risk in the system and give a feedback to the system designer.The main contents of this paper include:(1)We proposes an approach to simulate the dataflow behaviors base on CCSL.We extract the clock relations from SIGNAL designed system.And translate the clock relations into CCSL clock specifications.In CCSL environment,we can do verification and simulation on the clock relations in a visible way.Moreover,In our approach,the candidate execution platform can be taken into account through allocation.The result of the simulation offers a more valuable analysis and acceptable recommendation on the design of the whole system including the application and the architecture.(2)We proposes an approach to detect the boundedness issue in SIGNAL designed system based on LTS.First of all,we give a stateful semantic for each SIGNAL operation constructs by using LTS.Secondly,we discuss the boundedness problem in multi-clock system.At last,we present a boundedness detection algorithm based on such system.(3)Finally,we use the analysis method proposed in this thesis in a case study of an autopilot system.We design the system in SIGNAL,then verify the system in two way.We find the potential risk and repair it.The feasibility and effectiveness of the method presented in this thesis have been proved.