Detailed Requirement Of Embedded System Oriented Formal Modeling And Analysis

With a large number of software widely used in various industries,more and more industrial systems using the embedded software system to upgrade their industrial machinery.With the increasingly high performance of the hardware,people are willing to handle more complex tasks in modern industry.In this case,it is more and more important to ensure the safety of the safety-critical system.Both academics and industrial communities agree that rigorous requirements modeling and analysis can significantly contribute to the embedded software quality.However,applying formal methods to largescale industrial projects is a remaining challenge.The industrial engineers are suffering from the lack of automated engineering method-ologies to effectively conduct precise requirement models,and rigorously validate and verify the generated models.To tackle this challenge,we investigate the formal methods in industry and propose several methods in this paper.The contributions of this paper are summarized as below:·A light-weight requirement modeling language that supports domain fea-tures.we provide a systematic and automated solution to mitigate the challenges raised from the industry in terms of formal requirement modeling and V&V.In our strategy,AASRDL introduces a domain-specific modeling language with suf-ficient informal notations to construct the specification,;·An automated formal specification generation approach We present an au-tomated approach to generate a formal specification from property written by nat-ural language.We provide a semantic model of the safety property,use chunking and Dependency Parsing to collect the information to fill in the semantic model,And translate themm from the safety property to target formal language..·A systematic engineering approach FREPA to the formal FREPA presents a systematic engineering framework to integrate modeling and V&V technologies,and provides the automated analysis tool Aero Req for the requirements.FREPA consists of three major technologies: diagram-based validation,requirement sim-ulation,test case generation under the MC/DC coverage criteria and property checking?·A tool Aero Req that supports the automation of FREPA provides the au-tomated analysis tool Aero Req for the requirements.We design the tool to sup-port the usage of FREPA.We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems.The experimental results show that FREPA and the corresponding tool significantly facilitate formal modeling and V&V in the industry.Moreover,we also discuss the expe-riences and lessons gained from using FREPA in aerospace and aviation projects.