SOFL-based dependency graph generation for scheduling

摘要

In multi-task systems, different tasks work together to achieve desired functions. To guarantee the correctness of the functions, the tasks are required to be completed in specific orders. Violation of such orders will lead to the systems in unpredictable states, which may cause disasters. However, with the continuously increasing complexity in the developments of systems, to correctly generate the task dependency relation is becoming a challenge. A primary problem is the requirement specification may not be accurately and easily understood by the developers carrying out different tasks. To solve this problem, formal specification provides a feasible solution. However, some difficulties (e.g., high requirement of significant abstraction and mathematical skills) has hindered the widely usage of formal methods. To address these difficulties, SOFL, a formal engineering methodology, has been proposed. In this paper, we propose a method for generating task dependency relation based on SOFL specification. This method is demonstrated through a detailed case study of cruise control system. Moreover, we also provide a checking algorithm to check if there exist mistakes in the SOFL specification based on the transitivity of task dependency relation. We believe that these works provide a firm basis for the design of scheduling.