34IEEE SOFTWARE Published by the IEEE Computer Society 0740-7459/03/$17.00 © 2003 IEEEmonitoring, nuclear power plants, defense, mul-timedia, and process control are but a few ap-plication areas that employ computer softwarethat synchronizes and coordinates processes andactivities with timing constraints. Not only issoftware with hard timing requirements becom-ing increasingly important and pervasive, it isalso growing rapidly in size and complexity.In contrast, effective methods and tools forinspecting and verifying software’s timingproperties are conspicuously absent, despitean increasingly pressing need for them. This isdue primarily to the difficulty of verification.However, a preruntime scheduling approachcan help overcome this difficulty, making soft-ware timing properties much easier to inspectand verify.The verification problemWhat’s the main reason for this apparentdifficulty in developing effective methods andtools for verifying software timing properties?The problem is the complexity of software, es-pecially nonterminating concurrent software,and the complexity of such software’s possibletiming behaviors.Fundamental theoretical limitationsResearchers have found that the ability to ex-press even basic timing properties is a major fac-tor that keeps the complexity of a logical theoryor model high. Many of the logics and modelsthat researchers have proposed for modelingprograms’ timing properties are undecidable.1focusMaking Software TimingProperties Easier toInspect and VerifyThe world around us is depending more and more on computersystems that have timing requirements. Whether we fly on an air-plane, drive a car, make a phone call, undergo surgery at a hos-pital, or simply turn the lights on at home, we depend on real-time embedded software that must observe timing constraints either for oursafety or simply just to make things work. Avionics, air traffic control, au-tomobiles, telecommunications, medical applications such as intensive-care software inspectionSoftware with hard timing requirements should be designed using asystematic approach to make its timing properties easier to inspectand verify. Preruntime scheduling provides such an approach byplacing restrictions on software structures to reduce complexity.Jia Xu, York UniversityThis means that for a particular logic or model,no automatic method or tool can ever exist thatalways gives a definite answer to the question ofwhether the program satisfies the timing prop-erties. To make models and logics decidable, re-searchers can impose fairly severe restrictionssuch as limiting the system to a finite number ofstates, requiring the time domain to be discrete,and prohibiting quantification on time vari-ables. However, many logics and models willstill have high complexity.The models and logics that can express ba-sic timing properties are generally subject tothe state space explosion problem. That is, thestate space size we must explore to verify thoseproperties grows exponentially with the pro-gram description’s size. For example, to verifya program with 200 components, the statespace size that we might need to explore mightbe proportional to 2200! This exceeds the nor-mally available time and memory resources.To cope with state space explosion, all pro-gram verification methods use some form ofapproximation (for more information on cur-rent verification methods, see the sidebar).That is, the model only preserves selectedcharacteristics of the implementation whileabstracting away complex details. But then wehave the problem of deciding how to obtainsuch a model and how to prove that the modelfaithfully represents the original program, inthe sense that the model can answer correctlyall the correctness questions about the pro-gram. This can be more difficult than provingthe original program’s correctness.Complexity’s causesIf you take a hard look at what makes thetiming behaviors of existing real-time softwarecomplex, you might observe the following cur-rent practices in the design of real-time software:■ The software incorporates synchronizationmechanisms with complex timing behaviors.■ Real-time processes execute at randomtimes and preempt other processes at ran-dom points in time.■ Schedulers and other operating systemprocesses such as interrupt-handling rou-tines with complex behaviors affect appli-cation processes subtly and unpredictably.■ Programmers use ad hoc methods to dealwith additional constraints on the applica-tions such as precedence constraints, releasetimes that are not equal to the beginning oftheir periods, and low-jitter requirements.■ Programmers use priorities to deal withevery kind of requirement.■ To handle concurrent resource contention,programmers use task blocking, whichmight cause deadlocks.July/August 2003IEEE SOFTWARE 35Automatic methods or tools based on logics or models that are subject tostate space explosion (see the related section in the main article) can still beuseful where the program description is small. We can obtain small pro-gram descriptions when either the system represented by the program has asimple structure or the number of components is small. Hardware circuitsare often regular and hierarchical, and the number of components com-pared to software is small, so model checking has achieved a fair amountof success in checking the properties of hardware circuits.1However, for the reasons I mentioned earlier, formal verification methodshave not been used on the timing properties of actual software code. In par-ticular, large-scale, complex, nonterminating, and concurrent software has apressing need for this verification. But most research related to such verifica-tion has studied only simplified high-level abstractions of software such asspecifications, models, algorithms, or protocols that are only approximationsof the actual software. These abstractions do not take into account all the im-plementation details that might affect timing. Examples are theorem-provingtechniques that use PVS (Prototype Verification System) to analyze real-timescheduling protocols2and symbolic-model-checking techniques that checkhigh-level algorithms and protocols.3Most of model checking’s success is notso much in the formal verification of specifications but in the finding of bugsthat other informal methods such as testing and simulation don’t find, throughexploring only part of the state space.Because of the state-space-explosion problem, even state-of-the-art