Detection Algorithm And Its Implementation For Specific Execution Path In HSTM Software Design

Software systems play a very important role in the construction of cities in the future,Therefore,ensuring the correctness of functions is a key factor for software development.Hierarchical State Transition Matrix(HSTM)is a popular software design language and is widely used in the design of embedded software.For HSTM designs with complex hierarchies and invocation relationships,the execution paths are often difficult to track and debug,If paths(called change-reference paths),which lead from the first-time value-change of a variable to subsequent references of the variable can be automatically output,these paths can help HSTM designers better track changes in variables and analyze the causes of potential errors,help to develop functional and stable software.Currently,there is no change-reference path detection algorithm and tool implementation to HSTM design.Based on the state space exploration technology in formal verification,this thesis proposes a detection algorithm for the change-reference paths in HSTM software design;The problem of state space explosion in the exploration of state space(namely,the exploration cannot be completed within limited time with limited computing resources due to excessive states),uses Stateless Explicit State Exploration(SESE)and Bounded Context Switch(BCS)techniques to effectively alleviate the explosion of state space;In addition,deadlock checks and threshold checks are required on the HSTM design when detecting change-reference paths to avoid outputting erroneous results.The general steps of the algorithm are as follows:Firstly,the HSTM design is parsed and converted into a state transition system;secondly,the user-specified change-reference path specification is parsed;Then using the explicit state space exploration technology to perform path detection on the HSTM corresponding state transition system,The SESE technology memorizes the set of reachable states for each time step and BCS technique is used to limit the number of inter-process handovers that reach the current state set,and if a change-reference path is detected when a state is reached,a detailed transition path to the state is output.Otherwise,the output shows no.The change-reference path detection algorithm proposed in this thesis will be implemented in the Garakabu2 formal model checking tool developed earlier in our research group.In addition to the algorithm itself,The design implements the change-reference path specification parsing function and the shortest change-reference path output function.The experimental results show that the algorithm proposed in this thesis can effectively detect andoutput the change-reference path in complex HSTM software designs,and thus can play a significant role in helping the designer develop the correct HSTM software design.