The patent badge is an abbreviated version of the USPTO patent document. The patent badge does contain a link to the full patent document.
The patent badge is an abbreviated version of the USPTO patent document. The patent badge covers the following: Patent number, Date patent was issued, Date patent was filed, Title of the patent, Applicant, Inventor, Assignee, Attorney firm, Primary examiner, Assistant examiner, CPCs, and Abstract. The patent badge does contain a link to the full patent document (in Adobe Acrobat format, aka pdf). To download or print any patent click here.
Patent No.:
Date of Patent:
Feb. 04, 2003
Filed:
Aug. 17, 1999
Rajeev Alur, Ardmore, PA (US);
Mihalis Yannakakis, Summit, NJ (US);
Lucent Technologies Inc., Murray Hill, NJ (US);
Abstract
Model checking for message sequence charts (MSCs), message sequence chart graphs and hierarchical message sequence chart graphs (HMSCs) is provided. To verify the behavior of a given MSC, MSC graph and HMSC, a specification automaton is constructed. This specification automaton specifies the undesirable executions of the model under analysis. From the model under analysis, linearizations are defined from the model and a finite test automaton is constructed from the linearizations. The test automaton and the specification automaton are combined and it is determined whether there is an execution in the intersection. Where no state in the specification automaton is reachable from the test automaton, the model is verified.