Coping with incomplete information in Real Time Scheduling Verification
Maurizio Talamo, Andrea Callia D’Iddio, Christian H. Schunck, Franco Arcieri · Cineca Institutional Research Information System (Tor Vergata University) · 2013
The scheduling of processes is of strategic importance in many areas of software engineering. Verifying the correctness of scheduling is critical to ensure data integrity, process efficiency and system security. Therefore a scheduling must often be verified quick- ly or even in real time. In this case it may be inefficient or too re- source consuming to gather all the data about individual jobs. How- ever, missing information may prevent the unique identification of each job in the scheduling. In this paper we define a framework in which we model this information loss and we define methods and algorithms to check the correctness of a scheduling with regard to the order in which the jobs are executed in the presence of such ambigui- ties. Given a set of jobs and a specification, which is defined as a set of dependencies between the jobs, the task is to check if the order in which the jobs are scheduled satisfies the dependencies. We use par- tial order structures to mathematically model dependencies in the specification and in the order of execution of the scheduled jobs. If some jobs become indistinguishable due to information loss it is not possible to determine all the precedences between jobs and the notion of dominance is lost. Here we use abstraction mechanisms at the combinatorial level to obtain new notions of dominance that enable the comparison of ap- proximated partial orders. Based on these results, methods and algo- rithms are developed which can be used to test actual schedulings with regard to their specifications. Keywords—security, scheduling, smart cards, model checking.