WO2009058002A1

WO2009058002A1 - Method for an event-driven system

Info

Publication number: WO2009058002A1
Application number: PCT/NL2008/000243
Authority: WO
Inventors: Gürcan GÜLESIR; Louis Marie Johannes Bergmans; Mehmet Aksit
Original assignee: Universiteit Twente
Priority date: 2007-10-30
Filing date: 2008-10-30
Publication date: 2009-05-07
Also published as: NL1034599C2

Abstract

Method for an event-driven system with an initial state and at least one state transition from a source state to a destination state and an input alphabet with at least one input symbol, wherein an input symbol from the input alphabet is associated with a state transition, which state transition represents the transition from a source state to a destination state when the input symbol associated with the state transition is received, wherein at least one state transition is associated with all input symbols not already associated with one of the other state transitions sharing the same source state.

Description

Method for an event-driven system

The present invention relates to a method for an event-driven system. The present invention also relates to software for specifying software for an event-driven system. The present invention further relates to a system for specifying software for an event-driven system. In addition, the present invention relates to software specified as according to such a method. The present invention also relates to a data carrier comprising software according to the invention.

Photolithographic techniques are used in the semiconductor industry for the production of semiconductor products. During the photolithographic process patterns which must be arranged on or in the semiconductor material, wafer 21, are imaged on a light-sensitive layer on the semiconductor surface in a lithographic projection apparatus 20, a so-called wafer scanner. For this purpose light 27 from a laser source 26 is shone through a mask 23 on which the pattern for imaging is arranged, after which the light

27 incident through mask 23 is cast onto the light-sensitive layer on the semiconductor surface using a lens 28. Because simultaneous display of the fine structures of the pattern on the whole semiconductor surface is not possible, the semiconductor surface is divided into segments 29 which are illuminated successively. Nor is the whole of a single segment 29 illuminated simultaneously here, but a scanning movement is performed over the segment surface in order to eventually illuminate the whole segment surface. For this purpose mask 23 and the semiconductor surface are moved through light beam 27 in mutually opposite directions. Figure 2 also shows mask table 24, wafer table 22 and the pattern 25 to be imaged on mask 23.

Among other factors, the combination of the fine structures to be imaged and the high speed at which wafer scanner 20 operates in order to achieve the highest possible productivity result in a complex control of wafer scanner 20. A wafer scanner 20 typically comprises about 400 sensors and 300 actuators, and the software for controlling wafer scanner 20 comprises about fifteen million lines of source code . In order to keep the writing and maintaining of the source code manageable, use is made of various methods for structuring the source code and the writing and maintaining of the source code .

A frequently used method for structuring such extensive software systems is to sub-divide the software into a reactive part and a non-reactive part. The reactive part models different possible states of the system. This part receives events from, among other parts, the sensors and the non-reactive part. On the basis of these events the reactive part determines which control calls must be sent to the non-reactive part and into which new state the system enters. The non-reactive part is responsible for performing services which are called by the reactive part.

In most cases the reactive part can be modelled using a state chart. The state chart comprises a number of states corresponding with possible states of the system for controlling. State transitions always connect a source state to a destination state and have an associated input symbol which represents an event. When an event is received the state transition, which has the present state as source state and which is associated with the input symbol which represents the received event, determines the (destination) state to which the system moves. The subject of state charts itself will not be further elaborated here since the skilled person is familiar with state charts.

The complexity and size of software for the purpose of for instance controlling lithographic projection equipment entails modifications being made during the lifespan of the software, for instance in respect of software maintenance or product improvement, wherein errors may be made which result in defects in the software and the system.

Examples of such defects are : - an event call is defined but there is no corresponding event; - there is an event but the corresponding event call is not defined;

- the reactive part expects an event call which never takes place; - the target (function, method, procedure) of a control call is absent;

- the non-reactive part does not provide a required service.

It is self-evident that, as the software becomes larger and more complex, manual correction of such defects becomes an impossible task.

The present invention has for its object to provide a method with which determining of the above described defects is simplified, and such defects can even be prevented.

This object is achieved with the invention by- providing a method for an event-driven system with an initial state and at least one state transition from a source state to a destination state and an input alphabet with at least one input symbol, wherein an input symbol from the input alphabet is associated with a state transition, which state transition represents the transition from a source state to a destination state when the input symbol associated with the state transition is received, wherein at least one state transition is associated with all input symbols not already associated with one of the other state transitions sharing the same source state. The specifying of the event-driven system on the basis of a state chart makes it possible to formulate a precise specification of the system. In traditional state charts only a single input symbol is associated with a state transition. In the present invention an extra symbol is introduced, the context- sensitive wildcard, which can be associated with a state transition and which represents one or more input symbols, in contrast to the traditional method of a single input symbol being associated with a state transition. Which symbol is represented depends on the other state transitions which share the same source state as the state transition with the context-sensitive wildcard. The context-sensitive wildcard represents (for this state transition) all input symbols which are not already associated with one of these other state transitions, including input symbols which at the moment of specification did not (yet) form part of the input alphabet. It hereby becomes possible to define state transitions for input symbols which are introduced only a later time into the life cycle of the software, for instance as a result of the addition of new functionalities. A greater expressivity is hereby obtained than in traditional state charts .

The present invention further provides a method wherein at least one output symbol is associated with a state and wherein the method further comprises of : generating an output which is represented by the output symbol associated with the state of the event-driven system. In this way the specification of the output corresponds with a Moore machine .

The invention also provides a method wherein at least one output symbol is associated with a state transition, and the method further comprises of: generating an output which is represented by the output symbol associated with the state transition from the source state to the destination state when the event-driven system moves from a source state to a destination state. The output is now defined in a manner comparable to a Mealy machine.

The present invention provides a further method wherein the event-driven system comprises at least one sensor, and wherein at least one input symbol represents a representation of a detection by the sensor. It is possible in this manner for the system to react to measurements on objects for processing and to input provided by operators.

The present invention also provides a method wherein the event-driven system comprises at least one actuator and wherein the output symbol represents a control signal for the actuator. This extension enables the system to for instance manipulate objects for processing. In a further embodiment of the invention an event- driven system is provided, wherein the output symbol represents a reproduction by means of a reproducing device. The reproduction can be perceived by an operator who obtains information about the event-driven system on the basis of the reproduction information. Examples of such a reproduction are an alert that the system has completed an operation or a confirmation of an operating command.

Yet a further embodiment provides an event-driven system wherein the output symbol comprises the graphic representation of a symbol on a reproducing device. In a specific embodiment the reproducing device comprises a screen. This screen can for instance show the progress of the process executed by the event-driven system. The present invention further provides a method wherein the event-driven system is a lithographic projection apparatus. Using sensors the position and orientation of the wafer is for instance detected. Stepping motors are then for instance used to correctly position and orient the wafer. Another sensor makes it possible to establish whether contaminants are present on the mask, while an actuator is arranged to clean the mask if it is determined that the mask is not clean.

According to the invention a method is also provided wherein at least one input symbol represents a function call. This makes it possible to specify the sequence of activities. In another method a function call must here be understood in a broad sense. Finally, the source code of the function can alternatively by incorporated directly in the calling function, whereby one cannot speak of a function call. In this case function call must be understood to mean a block of statements which execute a clearly delimited task, such as for instance cleaning of the mask or positioning of the wafer. The invention further provides a method, further comprising of: specifying an event by specifying a condition under which the event occurs, comprising of defining at least one state and a state transition from a source state to a destination state with an input symbol from the input alphabet associated with the state transition; and of linking an event call to a state which represents a state of the event-driven system in which the event call takes place. The condition for the event comprises for instance a required series of operations which must be executed in a fixed sequence. In another example the condition comprises of a single detection by a sensor. In yet another example the condition comprises of a combination of detections by sensors and operations which must occur or take place in a determined sequence. This method has the additional advantage that the specification specifies the states in which an event call must be generated, whereby it becomes possible to have the implementation of the event call in the source code take place automatically. As will be shown later in this description with reference to the figures, a specific part of the source code of software can be associated with each state. This association also provides the option of determining the location in the source code where the event call must be generated. On the basis of the specification it is thus possible, without any contribution from a developer, to determine the location of the event call, and to actually insert this event call. The chance of an implementation which differs from the specification is hereby reduced, which decreases the risk of errors in the software .

The invention further provides a method wherein at least one state is defined as the final state, the method further comprising of: verifying whether a source code meets the given specification, comprising of: determining all possible flows of control of the source code; running through the state charts for each flow of control of the source code in order to determine whether the flow of control results in a state defined as a final state,- and determining whether a state defined as final state is reached for all possible flows of control. Source code is here understood to mean one or more series of related statements, irrespective of whether they implement a full application, a single module, a single library or a single function or routine .

According to this method, not only is a system specified but whether the given source code meets the specification is also verified. Possible variations from the specification can then be submitted to a developer in order to determine the problem: is the specification incorrect or is the implementation incorrect. The developer can then correct the specification or the source code, after which the source code is once again checked on the basis of the specification. This method has the advantage that the chance of detecting errors in the software is considerably increased.

The present invention also provides a method wherein the possible flows of control of the source code are modelled by a simplified control flow graph (SCFG) . The advantage of the SCFG modelling the possible flows of control is that this model does not depend on the programming language used to implement the system. It is hereby possible to make the algorithm for verifying the source code independently of the implementation language, whereby the algorithm can be used for more than a single implementation language .

The present invention further provides a method wherein the simplified control flow graph is constructed by first constructing an abstract syntax tree (AST) of the source code. In contrast to the SCFG, the AST is not implementation- independent but assists in the construction of the SCFG by providing a systematic, hierarchical division of the source code, on the basis of which the construction of the SCFG is facilitated.

The present invention also provides a method wherein the verification further comprises of constructing a mapping of a state with which an event is associated at a position in the source code for verifying; and of inserting an event call of the associated event at the mapped position. Use is preferably made in this step of the SCFG and the AST for finding the relation between the states from the specifications and the associated positions in the source code. On the basis of this relation the event call of an event is inserted in the source code, whereby the event calls establishes a link between the non-reactive part of the software and the reactive part. In a preferred embodiment of the invention this step is executed automatically in order to obviate the chance of an error by the developer .

In a preferred embodiment the present invention provides software for specifying software which, if run on a processor, executes a method as described above.

In another embodiment the present invention provides a system for specifying software according to a method as described. In an alternative embodiment the present invention provides software specified according to a method as described.

In yet another embodiment the invention provides a device comprising software specified according to a method as described.

The present invention further provides a data carrier comprising such software.

Further advantages and embodiments of the present invention will become apparent on the basis of the following description with reference to the figures, in which:

Figure 1 shows a schematic representation of software to which a method according to the present invention can be applied;

Figure 2 shows a schematic view of a wafer scanner, to the control software of which a method according to the present invention can be applied;

Figure 3 shows a simplified control flow graph of the wafer scanner to which a method of the present invention can be applied; , Figure 4 shows a schematic representation of a method according to the present invention;

Figure 5 shows a specification in accordance with a method according to the present invention; Figure 6 shows a specification in accordance with a method according to the present invention;

Figure 7 shows another specification in accordance with a method according to the present invention; Figure 8 shows yet another specification in accordance with a method according to the present invention;

Figure 9 shows an abstract syntax tree and a simplified control flow graph of a simplified function of control software of the wafer scanner to which a method according to the present invention can be applied; and

Figure 10 shows another abstract syntax tree of a simplified function of control software of the wafer scanner to which a method according to the present invention can be applied. Figure 11 shows yet another abstract syntax tree of a simplified function of control software of the wafer scanner to which a method according to the present invention can be applied.

In the control of wafer scanner 20 (figure 2) the successive positioning and scanning of each wafer segment 29 are the actual processing steps (processing) of wafer 21. Before these processing steps can actually begin, a number of preprocessing steps must be executed. Due to the great precision required in the production of the semiconductor products, relatively small irregularities and disruption can quickly result in defective products. In order to reduce the chance of defective products the mask 23 must be as clean as possible and the shape imperfections of wafer 21 must be known as well as possible. For this purpose preprocessing steps are executed, such as cleaning the mask and measuring the shape imperfections of wafer 21.

In order to produce the highest possible number of operating semiconductor products, the preprocessing steps are steps which must necessarily be carried out before the actual processing steps may be executed. This relation can be expressed in a state chart (figure 3) .

The wafer scanner begins initially 31 by transposing 32 to a state of readiness READY 33. In the state of readiness READY 33 the wafer scanner waits until a start event is received, which event can for instance be initiated by operating personnel pressing a button. Receiving the start event causes the wafer scanner to move 34 from the state of readiness READY 33 to the preprocessing state PREPROCESSING 35. As soon as the preprocessing is completed, a preprocessed event (preprocessed) ensures that transition 36 to the processing state PROCESSING 37 is initiated. As soon as the processing steps are also completed a processed event (processed) is generated, whereby wafer scanner moves 38 to the final state 39 and stops .

The most extensive method according to the invention basically comprises four steps (figure 4) . Step I : The software developer derives and specifies the compatibility constraints on the basis of, among other things, the software requirements, the state charts and the implementations of the various tasks of the software . Step II: The developer specifies the events and links the event calls.

Step III: A source code analyser analyses the source code on the basis of the specifications from steps I and II and produces inter alia a specification of the determined compatibility errors. The developer repairs the defect on the basis of this specification of a compatibility error. The source code analyser also produces a list of event points with corresponding event calls.

Step IV: On the basis of the source code and the list of event points with corresponding event calls produced by the source code analyser a source code to source code converter inserts the corresponding event call at each event point in the source code .

Once steps I and II have been executed, steps III and IV can be executed repeatedly after modification of the source code so as to guarantee that the software does not have the above stated defects . The four steps are discussed in more detail hereinbelow. Step I, the specification of the conditions, will be discussed in the following paragraphs .

Figure 5 shows an example of a specification of a compatibility constraint. The shown exemplary compatibility constraint Cl requires that the wafer be measured during the preprocessing of the wafer. The specification specifies the order of acceptable sequences of function calls. A large rectangle 50 represents the source code, designated with label 52 in this example of the preprocessing function preprocess . The label «from» is a specific example of a designation for the range of the applicability of the specification. In this case the label indicates that the specification applies to all calls from the preprocessing function preprocess . The preprocessing function has two states qθ, ql . A first state qθ is the initial state of the preprocessing function, this being designated with label «initial» 53. The state transition measureWafer 54 specifies a call to the measureWafer function. If the preprocessing function preprocess 52 calls the function measureWafer, state ql is then reached. The specification further shows two state transitions 56, 57 which are provided with a dollar sign ($) . The dollar sign is the context-sensitive wildcard which indicates that all symbols (function calls) are associated with this state transition, with the exception of the symbols already associated with a state transition which shares the same source state as the state transition with which the context-sensitive wildcard is associated. In this embodiment all function calls, except for the call to measureWafer, are thus associated with state transition 56 because measureWafer is already associated with state transition 54. All function calls are without exception further associated with state transition 57.

State ql is further provided with label «final» 55, which indicates that this state is a valid state for the function preprocess to end in. All function call sequences from the function preprocess which do not end in state ql do not therefore meet the specification of figure 5 because only state ql is a valid final state, i.e. provided with the label «final». The valid function call sequences in the function preprocess are all sequences in which the function measureWafer is called at least once. Possible other function calls in the sequence correspond with either state transition 56, if they precede the (first) function call measureWafer 54, or state transition 57 if they take place after the (first) function call.

A second compatibility constraint C2 for the preprocessing function is that the mask is optionally cleaned, for instance if a sensor, such as for instance a camera, has determined that mask 23 comprises contaminants, but that this cleaning may not take place after measuring of wafer 21. In the sequence of function calls this translates into the preprocessing function preprocess not being allowed (any longer) to call the cleaning mask function cleanReticle after the measure wafer function measureWafer has been called.

Note that this compatibility constraint C2 does not require wafer 21 having to be measured without limitation (irrespective of whether the mask is cleaned) .

This requirement is after all already set in compatibility constraint Cl. The specification of compatibility constraint C2 described hereinbelow will therefore not include this constraint, since compatibility constraint Cl is specified by its own specification. The skilled person will however appreciate that it is also unconditionally possible to construct a single specification in which both compatibility constraints Cl and C2 are specified.

Compatibility constraint C2 is specified as follows (figure 6) : The specification once again specifies function call sequences «from» (label 51) the preprocessing function preprocess (label 52) . The initial state is (label 63) state qθ, this state also being a valid final state. As long as the measure wafer function measureWafer has not yet been called from the preprocessing function preprocess, any random function can be called (including the cleaning mask function cleanReticle) , as indicated by state transition 65, with which the context-sensitive wildcard is associated. As indicated above, this specification does not require the presence of a call to the measure wafer function measureWafer in the function call sequence, since state qθ is a valid final state. If the preprocessing function preprocess does however call the measure wafer function measureWafer, state ql is then reached via state transition 66. If the cleaning mask function cleanReticle is called after the measure wafer function measureWafer has been called, state q2 is then reached via state transition 68. This state is not a valid final state, nor can a valid final state be reached from this state. Calling the cleaning mask function cleanReticle after calling the measure wafer function measureWafer thus produces a function call sequence which does not meet this specification. It is however permissible to call a function other than the cleaning mask function cleanReticle after the measure wafer function measureWafer has been called, as specified by state transition 57 with which the context-sensitive wildcard is associated. In the example of the preprocessing function preprocess the preprocessed event preprocessed is generated by calling the event call preprocessed () once the preprocessing function has been completed. How this event is specified in step II and how the event call is linked will be described hereinbelow.

The preprocessed event preprocessed is only generated if the final function call in preprocessing function preprocess is the call to the function measureWafer (figure 7) . An initial start is made in the initial state qθ. The label «initial-final» 73 specifies that state qθ is the initial state, but also a valid final state.

Note that states are specific to a single specification. States with the same designation in different specifications (and here different figures) are not necessarily the same identical states.

All function call sequences are valid sequences in this example, since all conditions, i.e. qθ and ql, are all final states. The intention of the specification in figure 7 is not to specify the valid function call sequences but only to specify when and in which state the preprocessed event call preprocessed () is called. This is specified by coupling this event to state ql by means of specifying the function call preprocessed () 79 as output symbol in state ql . Figure 7 now specifies that, each time state ql is reached, preprocessed event preprocessed is generated by calling preprocessed () . This is the case if the function measureWafer is called via state transitions 74 or 78. Any other random function call corresponds with the context- sensitive wildcard ($) and results, via one of the two state transitions 76 and 77, in state qθ in which no event is generated.

The above described compatibility constraints Cl and C2 and the specification of preprocessed event preprocessed can also be specified in a single specification (figure 8) . Function call sequences are once again shown «from» (label 51) the preprocessing function preprocess (label 52) . The initial state is qθ, as specified by label 83. State transition 84 specifies that all functions other than the measure wafer function measureWafer (but including cleaning mask function cleanReticle) may be called from qθ, wherein there is a return in each case to state qθ . State qθ is however not a valid final state (label 83) and in order to reach a valid final state measure wafer function measureWafer must be called (state transition 85) . In state ql the preprocessed event preprocessed is then generated by event call preprocessed {); label 86. Through further calls to the measure wafer function measureWafer and calls to functions other than the cleaning mask function cleanReticle and the measure wafer function measureWafer the respective states ql and q2 are reached, both of which are valid final states and therefore produce function call sequences which are in accordance with the specification. State q3 is however reached by a call to the cleaning mask function cleanReticle after the measure wafer function measureWafer has already been called. This state is not a valid final state and no valid final states can be reached from this state. A call to the cleaning mask function cleanReticle after the measure wafer function measureWafer has been called thus produces a call sequence which does not meet the specification. According to the specification the function call sequence must at least comprise a call to the measure wafer function measureWafer and no further calls to the cleaning mask function cleanReticle may take place after this function call. After each call to the measure wafer function measureWafer a preprocessed event preprocessed is further generated by calling the preprocessing function preprocessed ( ) ; .

In step III the source code is analysed on the basis of the specifications of steps I and II. For this example use is made of the following source code for the preprocessing function preprocess in programming language C:

1 void preprocess ( )

2 {

3 if ( ireticleClean)

4 { 5 cleanReticle ();

6 }

7 measureWafer ( ) ;

8 }

The source code analyser analyses the preprocessing function preprocess and constructs an abstract syntax tree (AST) (upper part of figure 9) . The node FDef represents a function definition. The nodes FCaIl represent function calls.

If the compatibility constraints and the events can be specified on the basis of function calls and the possible flow of control, only a part of the data from the AST is then necessary and on the basis of the AST a simpler model can be constructed which models only the function calls and the flow of control between the calls, i.e. a simplified control flow graph (SCFG) (lower part of figure 9) . An additional advantage of the SCFG compared to the AST is that the SCFG is not dependent on the chosen implementation language. The SCFG is derived by traversing the AST according to the depth-first search. The broken arrows indicate the corresponding points between the AST and the SCFG. The black dot to the left in the SCFG is the initial node, which represents the start of the implementation of the preprocessing function preprocess. The cleaning mask node cleanReticle 95 represents the call to the cleaning mask function cleanReticle. The measure wafer node measureWafer 97 represents the function call to the measure wafer function measureWafer. Finally, the black dot to the right represents the end of the implementation of preprocessing function preprocess. This dot is circled in order to indicate that it is an end node . The SCFG thus specifies the possible function call sequences which are possible on the basis of the source code.

Once the SCFG has been constructed, the source code analyser generates a list of possible function call sequences from the function for analysing, in this case preprocessing function preprocess . For this purpose the SCFG is traversed in accordance with the depth- first search. It can be readily appreciated in this case that there are only two possible sequences, i.e. the call to only the measure wafer function measureWafer and the call to the cleaning mask function cleanReticle followed by the call to the measure wafer function measureWafer. By running through the specifications on the basis of these two function call sequences (figure 8) the source code analyser determines that a valid final state is reached for all function call sequences, i.e. in this case state ql . The source code analyser concludes herefrom that the source code meets the compatibility constraints Cl and C2. If the source code analyser has found function call sequences which did not comply with one of the compatibility constraints (this being concluded because a valid final state is not reached in the specification) , an error message is then generated having therein the function call sequence (s) which does not comply with the constraints . For the purpose of the following step (step IV) a mapping of the states in the specification (figure 8) to the nodes in the SCFG is constructed during the comparison of the function call sequences possible on the basis of the SCFG. In the embodiment discussed here, state qθ from the specification is reproduced at node cleanReticle 95 and state ql is (according to both function call sequences) reproduced at node measureWafer 97.

In step IV a source code to source code transformation is executed in order to incorporate into the source code the event calls specified in step III. The event specifications specify (step II) for all event calls in which state these calls must take place. The location in the source code where the relevant event call must be inserted can be determined on the basis of the mapping of states to nodes in the SCFG determined in step III.

According to the specification of figure 8, the event call for the preprocessed event preprocessedO 86 is associated with state ql . In step III is determined that state ql corresponds with node measureWafer 97 in the SCFG (lower part of figure 9) . Node measureWafer 97 in the SCFG corresponds with the function call measureWafer () in the AST (upper part of figure 9) . The event call for the preprocessed event preprocessedO (figure 10) must thus be incorporated in the AST (figure 11) after the function call measureWafer () . This results in the event call for the preprocessed event preprocessed () also having to be incorporated in the source code after the function call measureWafer () . Step IV hereby produces the following source code:

1 void preprocessO

2 {

3 if ( ireticleClean)

4 { 5 . cleanReticle () ;

6 }

7 measureWafer ( ) ;

8 preprocessedO ; 9 }

With this final step the process is completed. A specification is formulated of the conditions which the preprocessing function preprocess must satisfy. An event has been specified. The source code is then verified on the basis of these specifications, and an event call for the specified event is finally added to the source code. The embodiments according to the invention described and shown in the description and figures are only exemplary embodiments. The skilled person will appreciate that many changes and modifications are possible which fall within the present invention. It will thus be apparent to the skilled person that the sequences of activities do not necessarily have to be defined by function calls, but that any other indication of delimitation of activities can be used for this purpose, such as for instance a comment designated in accordance with a predetermined convention. The protection sought is therefore not limited by the exemplary embodiments given here, but is defined by the following claims.

Claims

1. Method for an event-driven system with an initial state and at least one state transition from a source state to a destination state and an input alphabet with at least one input symbol, wherein an input symbol from the input alphabet is associated with a state transition, which state transition represents the transition from a source state to a destination state when the input symbol associated with the state transition is received, wherein at least one state transition is associated with all input symbols not already associated with one of the other state transitions sharing the same source state.

2. Method as claimed in claim 1, wherein at least one output symbol is associated with a state and wherein the method further comprises of : generating an output which is represented by the output symbol associated with the state of the event-driven system.

3. Method as claimed in claim 1, wherein at least one output symbol is associated with a state transition, and the method further comprises of : generating an output which is represented by the output symbol associated with the state transition from the source state to the destination state when the event-driven system moves from a source state to a destination state.

4. Method as claimed in claim 1, 2 or 3, wherein the event-driven system comprises at least one sensor, and wherein at least one input symbol represents a representation of a detection by the sensor.

5. Method as claimed in claim 2, 3 or 4 , wherein the event-driven system comprises at least one actuator, and wherein the output symbol represents a control signal for the actuator.

6. Method as claimed in any of the claims 1-5, wherein the event-driven system is a lithographic projection apparatus (20) .

7. Method as claimed in any of the claims 1-6, wherein at least one input symbol represents a function call.

8. Method as claimed in any of the claims 1-7, further comprising of: specifying an event by specifying a condition under which the event occurs, comprising of defining at least one state and a state transition from a source state to a destination state with an input symbol from the input alphabet associated with the state transition; and linking an event call to a state which represents a state of the event-driven system in which the event call takes place.

9. Method as claimed in claim 8, wherein at least one state is defined as final state, the method further comprising of: verifying whether a source code meets the specification given as according to claim 8, comprising of: determining all possible flows of control of the source code ; running through the state charts for each flow of control of the source code in order to determine whether the flow of control results in a state defined as a final state; and determining whether a state defined as final state is reached for all possible flows of control.

10. Method as claimed in claim 9, wherein the possible flow of control of the source code is modelled by a simplified control flow graph (SCFG) .

11. Method as claimed in claim 10, wherein the simplified control flow graph is constructed by first constructing an abstract syntax tree of the source code.

12. Method as claimed in claim 9, 10 or 11, wherein the verification further comprises of constructing a mapping of a state with which an event is associated at a position in the source code for verifying; and inserting an event call of the associated event at the mapped position.

13. Software for specifying software which, if run on a processor, executes a method as claimed in any of the claims 1-12.

14. System for specifying software according to a method as claimed in any of the claims 1-12.

15. Software specified according to a method as claimed in any of the claims 1-12.

16. Device comprising software as claimed in claim 15.

17. Data carrier comprising software as claimed in claim 13.

18. Data carrier comprising software as claimed in claim 15.