Title of Invention

METHOD AND SYSTEM OF VERIFYING THE ROBUSTNESS OF A MODEL OF A PHYSICAL SYSTEM

Abstract

The invention provides a system and a method for verifying the robustness of a model of a physical system, the method comprising the following steps: defining a first model (10) of the physical system comprising a set (12) of components (12a, 12b, 12c) and at least one input interface (14) for inserting input values, said first model being defined in a formal language describing the behavior and the function of each of said components; defining in the formal language a determined property that must be satisfied by the model of the physical system; defining in the formal language a second model (20) corresponding to the first model and enriched by a fault injection mechanism (22); and using formal proof means to search automatically for a combination of injected faults and/or input values that causes said determined property to fail.

Full Text

FORM 2 THE PATENTS ACT, 1970 (39 Of 1970) & The Patents Rules, 2003 PROV4SIONAL / COMPLETE SPECIFICATION (See section 10 and rule 13) 1. TITLE OF THE INVENTION : "CHECKING THE ROBUSTNESS OF A MODEL OF A PHYSICAL SYSTEM" 2. APPLICANT (S) (a) NAME : HISPANO SUIZA (b) NATIONALITY : French (C)ADDRESS : 18 boulevard Louis Seguin 92700 COLOMBES FRANCE 3. PREAMBLE TO THE DESCRIPTION PROVISIONAL The following specification describes the invention COMPLETE The following specification particularly describes the invention and the manner in which it is to be performed. 4. DESCRIPTION (Description shall start from next page) 5. CLAIMS (not applicable for provisional specification. Claims should start with the preamble - "l/we claim" on separate page) 6. DATE AND SIGNATURE (to be given at the end of last page of specification) 7. ABSTRACT OF THE INVENTION (to be given along with complete specification on separate page) 2 Title of the invention Checking the robustness of a model of a physical system. Field of the invention 5 The present invention relates to the field of checking the robustness of a model of a physical system in the face of faults appearing. Prior art 10 In numerous industries, such as the aviation or space industries, it is common practice to rely on models of systems. For example, a model is designed of a physical system that is to accomplish some given mission, and the model is used in order to evaluate interference 15 between the system and its environment. This is done using either hardware means or software means. In particular, fault detection logic, reconfiguration logic, and component redundancy are used in order to make a system tolerant to faults. 20 Unfortunately, it is practically impossible for a model to take account of all eventualities. It often happens that some particular scenario is forgotten, or that a sequential logic error is made, such that some sequence or particular combination of faults can still 25 cause the system to fail. In order to solve those problems, real systems are bench tested in order to verify their robustness. However, on discovering a defect in a real system, it is necessary to redesign the system, which implies major new 30 engineering costs, hardware and software reverse engineering, and a major loss of time. Object and summary of the invention An object of the present invention is thus to solve 35 the above-mentioned problems by proposing a method of verifying the robustness of a model of an electronic system when faced with faults. 3 To this end, the invention provides a method of verifying the robustness of a model of a physical system, the method being characterized in that it comprises the following steps: 5 • defining a first model of the physical system comprising a set of components and at least one input interface for inserting input values, said first model being defined in a formal language describing the behavior and the function of each of said components; 10 • defining in the formal language a determined property that must be satisfied by the model of the physical system; • defining in the formal language a second model corresponding to the first model and enriched by a fault 15 injection mechanism; and • using formal proof means to search automatically for a combination of injected faults and/or input values that causes said determined property to fail. Thus, the second model enables a physical system to 20 be designed that is robust in the face of faults, and for this to be achieved in particular prior to making the system, thus making it possible to reduce the cost of developing it. This method makes it possible to verify the 25 properties of the system by taking account of various combinations of faults and/or input values to the system. It also makes it possible to make a system that is of very high quality and good safety by exhaustively verifying any conceivable fault or sequence of faults. 30 According to a feature of the invention, the fault injection mechanism includes injecting at least one fault into the second model via a fault input interface. According to another feature of the invention, the fault injection mechanism further comprises the 35 description in the formal language of the effect(s) of said at least one fault on the function or the behavior of each of the components of said electronic system. 4 The determined property is considered as being true relative to the second model when the formal proof means can find no combination of injected faults and/or input values that causes said determined property to fail. In 5 which case, the model of the physical system is considered as being robust relative to said determined property. The determined property is considered as being false relative to the second model when the formal proof means 10 finds at least one combination of injected faults and/or input values that causes' said determined property to fail. In which case,(said combination of injected faults and/or input values causing the determined property to fail corresponds to a scenario that can enable the model 15 of the physical system to be corrected to make it more robust. Advantageously, the combination of faults is selected from a predefined set of faults. The determined property expresses a state or a 20 behavior of said physical system. It may be a safety property of said physical system. Brief description of the drawings Other features and advantages of the method and the 25 system of the invention appear more clearly on reading the following description given by way of non-limiting indication and made with reference to the accompanying drawings, in which: • Figure 1 is a perspective view of hardware means 3 0 implemented in the method or system of the invention; • Figure 2 is a highly schematic diagram of a first model for designing a physical system in accordance with the invention; • Figure 3 is a flow chart showing the main steps 35 for determining the validity of the first model shown in Figure 2; 5 • Figure 4 is a highly schematic diagram showing a second model corresponding to the first model of the physical system enriched by a mechanism for injecting faults in accordance with the invention; 5 • Figure 5 is a flow chart showing the main steps for verifying the robustness of a model of the physical system faced with the appearance of faults, in accordance with the invention; • Figure 6 is a highly schematic diagram of an 10 example of a first model of an electronic system modeling a first computer, a second computer, and a harness, in accordance with the invention; • Figure 7 is a highly schematic diagram showing a second model corresponding to the first model of Figure 6 15 enriched by a fault injection mechanism; and • Figure 8 is a highly schematic diagram of the Figure 7 mechanism for injecting faults. Detailed description of embodiments 20 Figure 1 shows a system that can be used for modeling a physical system. The system comprises a workstation or computer 1 used for running a computer program designed to implement the method of the invention. 2 5 The computer 1 comprises the hardware means that are conventionally to be found with this type of apparatus. More particularly, the computer comprises a central unit 2 which executes sequences of instructions of the program in accordance with the method of the invention, a central 3 0 memory 3 which stores data and the program that is being executed, digital data storage media (hard disk, compact disk (CD) 4, floppy disk, ...) for long-term storage of the data and programs in use, input peripherals (keyboard 5, mouse 6, . . . ) , and output peripherals (screen 7, 35 printer, ...) for enabling the model of the physical system to be viewed. 6 In accordance with the invention, Figure 2 shows a first model 10 for designing a physical system. The physical system may, for example, be an electronics system that, once made, is to support a given application 5 such as monitoring or controlling equipment for regulating an engine. The first model 10 comprises a set 12 of components 12a, 12b, 12c in communication with one another, at least one input interface 14 for inserting input values, and at 10 least one output interface 16. Naturally, the set 12 of components may be defined on a scale or level of abstraction that depends on the precision or the specificity and the model of the physical system. This first model 10 is a numerical model 15 representing the architecture of the physical system to be made. It is defined in a formal language of the "Signal" type comprising an alphabet or variables, logical quantifiers, and logical connectors, thus describing the behavior and the function of each of the 20 components 12a, 12b, and 12c. The first model 10 thus enables the physical system to be represented dynamically. Figure 3 is a flow chart showing the main steps for determining the validity of the first model 10. 25 In step El, the first model is defined in a formal language. Then, in step E2, a determined property that must be satisfied by the model of the physical system is also defined in the formal language. The formal description 30 of the property consists in defining the event that corresponds to said property and in encoding this event, e.g. in the Signal language, on the basis of the variables or signals of the model. The determined property is in general a safety property of the type 35 "such an event will never happen", but it may also be a responsiveness property of the type "from such a state, it is possible to reach such an other state at the end of 7 a finite length of time". This property must then satisfy or describe a characteristic of the first model. The formal language has formal proof means such as the "formal prover" or "checker" m the SILDEXTM software, 5 for semantically verifying the truth of the determined property relative to any value or combination of values input into the first model. Thus, step E3 is a test of the truth of the determined property relative to any combination of input 10 values. In this step, an automatic search is made by the formal proof means for a combination of input values that causes this determined property to fail. If the formal proof means can find no combination of input values that causes the determined property to fail, 15 then in step E4, the first model 10 is considered as being valid relative to said property. In contrast, if the determined property is considered as being false, i.e. if the formal proof means in step E3 finds at least one combination of input values 20 that causes this determined property to fail, then the method moves onto step E5. In step E5, a diagnosis is provided, comprising the sequences of input values that cause the determined property to fail. 25 In step E6, depending on the diagnosis provided in the preceding step, the first model 10 is either corrected so that the determined property is satisfied, or else it is affirmed that the combination of input values found by the formal proof means is most 30 improbable. In accordance with the invention, Figure 4 is a highly diagrammatic view of a second numerical model 2 0 corresponding to the first model 10 of the physical system and enriched by a fault injection mechanism 22. 35 The second model 20 differs from the first model 10 in that, in addition to the set 12 of the components 12a, 12b, and 12c, and the input and output interfaces 14 and 8 16, it further comprises a fault injection mechanism 22 comprising a fault input interface 24 through which at least one fault or combination of faults is injected, together with fault applier means 26. 5 The fault or combination of faults is selected from a set of predefined faults. The effect of each fault on the behavior of the second model 20 is modeled in a formal language and the consequence of a fault on a given component is described in a behavior diagram for said 10 component. All known possible faults on the least component of the second model 2 0 are listed and are thus put into the behavior diagram of each component in a database stored in the central memory 3 of the workstation or computer 1, for example. 15 In other words, the fault injection mechanism 22 includes the description in a formal language of the effect(s) of any fault on the function or the behavior of each of the components 12a, 12b, and 12c of the second model 20 modeling the physical system. 20 Thus, the second model 20 corresponds to the first model 10 increased by as many additional Boolean inputs and processes as there are associated with foreseeable faults. The input of one particular fault can then take one of two values "false" or "true". For example, the 25 value "false" can correspond to the state "no fault injection", and the value "true" can correspond to the state "fault injection". When all of the inputs of the fault interface 24 are false, then the second model 2 0 operates under nominal 30 condition. when a fault input is true, it triggers the logic for applying the fault to the component concerned in application of the behavior diagram for that component. In addition, when a fault input is free, then the 35 formal proof means can introduce a fault at any time in order to seek a sequence or combination of faults and/or 9 of input values that can cause the determined property to fail. The formal proof means is a tool that applies logic rules to axioms and/or behavior diagrams for the 5 components 12a, 12b, and 12c of the second model 20 until it obtains a formula describing the determined property. This formal proof tool can be provided by software of the SILDEX type which at all instants during a stimulation can apply a fault to a component or a 10 function of the second model 20 via the fault injection mechanism 22. Specifically, in order to prove a determined property of the second model 20, a dynamic compilation in formal language of the SILDEX type is launched. If the 15 compilation succeeds, then the determined property is validated. Otherwise, the formal proof means gives a scenario including a sequence of faults and/or input values that lead to the system being modeled occupying a state that contradicts said property. 2 0 Figure 5 is a flow chart illustrating the main steps for verifying the robustness of a model of the physical system faced with the appearance of faults. In step Ell, the second model 20 is defined in a formal language to correspond to the first model 10 25 enriched by the fault injection mechanism 22. Thereafter, it is verified whether the determined property defined in step E2 of the flow chart of Figure 2 and that has already been verified as being true for the first model 10 (step E4) is still true for the second 3 0 model 20. During step E13, the truth of the determined property is tested relative to any combination of injected faults and/or input values. During this step, an automatic search is made by the formal proof means for 35 a combination of injected faults and/or input values that causes said determined property to fail. 10 If the formal proof means cannot find any combination of injected faults and/or input values that causes said determined property to fail, then the property is considered as being true, and consequently, 5 in step E14, the model of the physical system is considered as being robust in the face of faults relating to the determined property. In contrast, if during step E13 the formal proof means finds at least one combination of injected faults 10 and/or input values that causes said determined property to fail, then said property is considered as being false, and consequently in step E15, a diagnosis is provided by the formal proof means. This diagnosis comprises the scenario or sequence of inputs via the fault and input 15 value inputs 24 and 14 that leads to the unwanted situation. In step E16, the diagnosis is analyzed, i.e. the sequence of operations on the second model 20 is examined as are the instants at which the or each fault was 20 injected. This analysis serves to revise the design of the model of the physical system or on the contrary to affirm that the scenario found by the formal proof means is improbable. Figures 6 to 8 show a simplified example of 25 verifying the robustness of a model of a physical system. In this example, the physical system that is being designed is an electronic system comprising two computers for controlling an airplane engine. In normal operation, only one computer controls the engine and a dialog or an 30 exchange of data takes place between the two computers. Thus, in the event of one of the computers failing, the second computer must start running in single-computer mode. In this example, loss of the system corresponds to both computers being simultaneously either faulty, or 35 passive, or active. Thus, Figure 6 shows an example of a first model 110 of the physical system modeling a first computer 112a 11 having a first input interface 114a and a first output interface 116a, a second computer 112b having a second input interface 114b and a second output interface 116b, and an inter-computer harness 112c having connection 5 wires enabling the dialog or the exchange of data to take place between the first and second computers 112a and 112b. Arrow Fl designates signals or data (written S_l_2 in the Signal language) transmitted by the first computer 112a to the second computer 112b, and arrow F2 represents 10 the signals or data (written S_2_l in the Signal language) going from the second computer 112b to the first computer 112a. Figure 7 shows a second model 12 0 of the physical system corresponding to the first model 110 of Figure 6, 15 and enriched by a fault injection mechanism 122 comprising a fault input interface 124 and a fault applier means 126. In this example, the fault applier means 12 6 comprises switch means simulating a fault in a single connection wire that goes open circuit, or wires 2 0 that are short circuited, or the harness 112c being unconnected. Arrow Fla represents signals S_l_2 leaving the first computer 112a and arrow Fib represents signals S_2_l_v entering the second computer 112b after passing through the fault applier means 126. Arrow F2b 25 designates the signals S_2_l leaving the second computer 112b, and arrow F2a represents the signals S_l_2_v entering the first computer 112a after passing through the fault applier means 126. When there is no fault, the signal leaving the first or second computer 112a or 112b 3 0 enters unchanged into the second or first computer 112b or 112a respectively. In contrast, in the event of a fault, the signal leaving one or the other of the computers 112a, 112b does not reach its destination. In the Signal language this is represented by the following 35 equations: S_l_2_v = S_l_2 when not fault S__2_l_v = S_2_l when not fault 12 Figure 8 is a highly schematic diagram showing the fault injection mechanism and in particular the fault applier means 126 of Figure 7. The fault applier means 126 comprises a first fault input 124a corresponding to 5 "harness not connected" and a second fault input 124b corresponding to "dialog wire interrupted". The first and second fault inputs 124a and 124b are connected to the inputs of a logic OR gate 132 whose output is applied to a first connection/disconnection means 134 for 10 transferring or not transferring data from the first computer 112a to the second computer 112b, and to a second connection/disconnection means 13 6 for transferring or not transferring data from the second computer 112b to the first computer 112a. 15 The fault inputs can be thought of as buttons for applying faults to the modeled components. Thus, during simulations, it is possible to introduce faults at desired instants. When the formal proof means undertakes the automatic 20 search for a combination of injected faults and/or input values that causes the determined property to fail, the inputs set to the "false" value are not involved in the search for a counter-example scenario. Only the free inputs are involved in this search. 25 Thus, when no fault is injected into the first connection means 134, the input signals SA_e, SB_e, SC_e, and SD_e are equal respectively to the output signals SA_s, SB_s, SC_s, and SD_s of the connection means 134. Under such circumstances, the signals SA_1_2, SB_1_2, 30 SC_1_2, and SD_1_2 transmitted from the first computer 112a are enabled by the first connection means 13 4 and are forwarded to the second computer, being written respectively as follows: SA_l__2_v, SB_l_2_v, SC_l_2_v, and SD_l_2_v. 35 Similarly, when no fault is injected into the second connection means 13 6, the input signals SE_e, SF_e, SG_e, and SH_e equal respectively to the output signals SE_s, 13 SF_s, SG_s, and SH_s from the connection means. Under such circumstances, the signals SE_1_2, SF_1_2, SG_1_2, and SH_1_2 transmitted from the first computer 112b are enabled by the second connection means 13 6 to be sent to 5 the first computer 112a respectively as follows: SE_l_2_v, SF_l_2_v, SG_l_2_v, and SH_l_2_v. When the first fault input 124a corresponding to "harness not connected" and/or the second fault input 124b corresponding to "dialog wire interrupted" is free, 10 the formal proof means or prover can introduce a harness disconnection and/or a wire disconnection at any time. Under such circumstances, the signal(s) transmitted by one of the computers 112a, 112b cannot reach the other computer. 15 After initialization, the above example can be written in the Signal language as follows: process xxx_process_sildex_l= (? boolean SA_e, fault, SB_e, SC_e, SD_e; | boolean SA_s, SB_s, SC_s, SD_s;) 2 0 (| (| SA_s = SA_e when not fault SB_s = SB_e when not fault SC_s = SC_e when not fault SD_s = SD_e when not fault fault"= SA_e"= SB_e"= SC_e"= SD_e 25 |) I ) ; process xxx_process_sildex_2= (? boolean SE_e, fault, SF_e, SG_e, SH_e; | boolean SE_s, SF_s, SG_s, SH_s;) 3 0 (| (| SE_s = SE_e when not fault SF_s = SF_e when not fault SG_s = SG_e when not fault SH_s = SH_e when not fault faults SE_e~= SF_e~= SG_e"= SH_e 35 I); 14 In general, in the model of a physical system having two computers, it is possible to examine the following two properties: "the model of the system cannot find itself with two computers active" and "the model of the 5 system cannot find itself with two computers passive". In addition, it is possible to envisage modeling the situation in the presence of a single fault when the system is switched on. Under such circumstances, it is possible to verify whether any single fault present at 10 switch-on might not cause the system to take on the above-specified properties. Furthermore, it is possible to envisage modeling the presence of a single fault in operation, with both computers starting up simultaneously. Under such 15 circumstances, it is assumed that each single fault can be introduced at any instant. To do this, the fault input in question can be left free while keeping all the others false. Faults can be selected from a set of predefined 2 0 faults comprising the following faults: no fault; autotest fail; open circuit; short circuit; break in sending; harness not connected; synchronization fault; NVM fault forced to false; NVM fault forced to true; PPAVM signal fault forced to false; PPAVM signal fault 25 forced to true; PPAVMTPB; computer fault; PH signal fault forced to false; PH signal fault forced to true; etc. Thus, the invention makes it possible to verify the robustness of the model in the face of faults, prior to making the physical system, thereby enabling a system to 3 0 be made that presents good safety while reducing the cost of developing the system. Naturally, the invention also makes it possible to verify the robustness of a physical system that has already been made. Under such circumstances, the 35 physical system is modeled using a model in formal language and the robustness of the model of the physical system is checked in the manner described above with 15 respect to criteria defined by determined properties for the system when faced with failures. 16 CLAIMS 1. A method of verifying the robustness of a model of a physical system, the method being characterized in that it comprises the following steps: 5 • defining a first model (10) of the physical system comprising a set (12) of components (12a, 12b, 12c) and at least one input interface (14) for inserting input values, said first model being defined in a formal language describing the behavior and the function of each 10 of said components; • defining in the formal language a determined property that must be satisfied by the model of the physical system; • defining in the formal language a second model 15 (20) corresponding to the first model and enriched by a fault injection mechanism (22); and • using formal proof means to search automatically for a combination of injected faults and/or input values that causes said determined property to fail. 20 2. A method according to claim 1, characterized in that the fault injection mechanism (22) includes injecting at least one fault into the second model (20) via a fault input interface (24). 25 3. A method according to claim 2, characterized in that the fault injection mechanism (22) further comprises the description in the formal language of the effect(s) of said at least one fault on the function or the behavior 30 of each of the components of said electronic system. 4. A method according to claim 1, characterized in that the determined property is considered as being true relative to the second model (20) when the formal proof 35 means can find no combination of injected faults and/or input values that causes said determined property to fail. 17 5. A method according to claim 4, characterized in that the model of the physical system is considered as being robust relative to said determined property. 5 6. A method according to claim 1, characterized in that the determined property is considered as being false relative to the second model (20) when the formal proof means finds at least one combination of injected faults 10 and/or input values that causes said determined property to fail. 7. A method according to claim 6, characterized in that said combination of injected faults and/or input values 15 causing the determined property to fail corresponds to a scenario that can enable the model of the physical system to be corrected to make it more robust. 8. A method according to any one of claims 1 to 7, 20 characterized in that the combination of faults is selected from a predefined set of faults. 9. A method according to any one of claims 1 to 8, characterized in that the determined property expresses a 25 state or a behavior of said physical system. 10. A method according to claim 9, characterized in that the determined property is a safety property of said physical system. 30 11. A system for verifying the robustness of a model of a physical system, the system being characterized in that it comprises: • a first model (10) defining the physical system 35 and comprising a set (12) of components (12a, 12b, 12c) and at least one input interface (14) for inserting input values, said first model being defined in a formal 18 language describing the behavior and the function of each of said components: • a predetermined property defined in the formal language that must be satisfied by the model of the 5 physical system; • a second model (20) defined in the formal language, the second model corresponding to the first model enriched by a mechanism for injecting faults (22); and 10 •formal proof means for searching automatically for a combination of injected faults and/or input values that causes said determined property to fail. 12. A system according to claim 11, characterized in that 15 the mechanism for injecting faults (22) comprises a fault input interface (24) and fault applier means (26). 13. A system according to claim 11 or claim 12, characterized in that the physical system is an 20 electronic system comprising two computers for controlling an airplane engine. 14. A method and a system of verifying the robustness of a model of a physical system substantially as herein described and illustrated with reference to the accompanying drawings. Dated this 02nd day of May 2005 RAJESHWARI H. OF K & S PARTNERS ATTORNEY FOR THE APPLICANTS 19 ABSTRACT The invention provides a system and a method for verifying the robustness of a model of a physical system, 5 the method comprising the following steps: defining a first model (10) of the physical system comprising a set (12) of components (12a, 12b, 12c) and at least one input interface (14) for inserting input values, said first model being defined in a formal language describing the 10 behavior and the function of each of said components; defining in the formal language a determined property that must be satisfied by the model of the physical system; defining in the formal language a second model (20) corresponding to the first model and enriched by a 15 fault injection mechanism (22); and using formal proof means to search automatically for a combination of injected faults and/or input values that causes said determined property to fail.

Documents:

542-MUM-2005-ABSTRACT(13-4-2009).pdf

542-mum-2005-abstract(granted)-(16-10-2009).pdf

542-mum-2005-abstract.doc

542-mum-2005-abstract.pdf

542-MUM-2005-CANCELLED PAGES(13-4-2009).pdf

542-MUM-2005-CLAIMS(13-4-2009).pdf

542-mum-2005-claims(granted)-(16-10-2009).pdf

542-mum-2005-claims.doc

542-mum-2005-claims.pdf

542-MUM-2005-CORRESPONDENCE(13-4-2009).pdf

542-mum-2005-correspondence(23-4-2007).pdf

542-mum-2005-correspondence(ipo)-(21-10-2009).pdf

542-mum-2005-correspondence-received-ver-020505.pdf

542-mum-2005-correspondence-received-ver-020805.pdf

542-mum-2005-correspondence-received-ver-060705.pdf

542-mum-2005-correspondence-received-ver-090805.pdf

542-mum-2005-correspondence-received-ver-110705.pdf

542-mum-2005-description (complete).pdf

542-MUM-2005-DESCRIPTION(COMPLETE)-(13-4-2009).pdf

542-mum-2005-description(granted)-(16-10-2009).pdf

542-MUM-2005-DRAWING(13-4-2009).pdf

542-mum-2005-drawing(granted)-(16-10-2009).pdf

542-mum-2005-drawings.pdf

542-mum-2005-form 1(11-7-2005).pdf

542-MUM-2005-FORM 1(13-4-2009).pdf

542-mum-2005-form 1(20-10-2009).pdf

542-mum-2005-form 18(19-4-2007).pdf

542-mum-2005-form 2(13-4-2009).pdf

542-mum-2005-form 2(granted)-(16-10-2009).pdf

542-MUM-2005-FORM 2(TITLE PAGE)(13-4-2009).pdf

542-MUM-2005-FORM 2(TITLE PAGE)-(13-4-2009).pdf

542-mum-2005-form 2(title page)-(granted)-(16-10-2009).pdf

542-MUM-2005-FORM 26(13-4-2009).pdf

542-mum-2005-form 26(14-10-2009).pdf

542-mum-2005-form 26(23-4-2007).pdf

542-MUM-2005-FORM 3(13-4-2009).pdf

542-mum-2005-form 3(2-8-2005).pdf

542-mum-2005-form 3(3-5-2005).pdf

542-mum-2005-form 3(9-8-2005).pdf

542-mum-2005-form-1.pdf

542-mum-2005-form-2.doc

542-mum-2005-form-2.pdf

542-mum-2005-form-3.pdf

542-mum-2005-form-5.pdf

542-MUM-2005-OTHER DOCUMENT(13-4-2009).pdf

542-mum-2005-petition under rule 137(13-4-2009).pdf

542-mum-2005-specification(amended)-(13-4-2009).pdf

abstract1.jpg