Proposing a Formal Method to Reduce RTS Logical Model Complexity

Complex real time systems (RTS) often come with many requirements, which have a difficult description with a large number of scenarios. In order to control this complexity and improve the system QoS, a formal method was applied to decrease the complexity of logical model descriptions, related to state diagrams. The approach introduces a mapping of states diagrams to automata, in order to bring in formal methods into the system development process. By applying the Myhill Nerode minimization process for automata, the authors could recognize some decrease of the model complexity. The case study validates the approach by reducing the initial state diagram of a RTS from 5 states and 40 transitions to 1 state with 5 transitions. This finding can motivate the software engineers´ community to research formal methods that could be applied to software development processes.