Kenneth Mark Thompson

US Patent:

6353896, Mar 5, 2002

Filed:

Dec 15, 1998

Appl. No.:

09/211967

Inventors:

Gerard Johan Holzmann - Murray Hill NJ
Kenneth Lane Thompson - Watchung NJ
Philip Steven Winterbottom - Watchung NJ

Assignee:

Lucent Technologies Inc. - Murray Hill NJ

International Classification:

G06F 1136

US Classification:

714 38, 717 1

Abstract:

A technique for testing event driven software. In accordance with the technique, the source code of the event driven software is directly converted to an automation based model useful in verifying that the program code complies with the desired properties defined by the user. More particularly, the event driven system program code is translated into a target language for a particular model checker. Such a translation results in a model which contains statements directed at whether execution of the program code will affect the behavior of the event driven system. Thus, this model extraction process can be used as input to a logic model checker for determining whether event driven system complies with the desired correctness properties specified by the user. Advantageously, the model extraction process and application of the model checker occurs in a direct and dynamic fashion from the subject event driven system program code without the need for user intervention.

US Patent:

54577969, Oct 10, 1995

Filed:

Jun 10, 1994

Appl. No.:

8/259262

Inventors:

Kenneth L. Thompson - Watchung NJ

Assignee:

AT&T IPM Corp. - Coral Gables FL

International Classification:

G06F 1730

US Classification:

395600

Abstract:

A file system which has component file systems including a primary file system which is react/write and a number of dump file systems which are read only. Each dump file system is created from the primary file system by means of a dump operation and conserves the state of the primary file system at the time the dump operation was performed. Component file systems share read only storage elements with older component file systems. The file system is implemented on a system including a file server, a magnetic disk mass storage device, and an optical write once-read many (WORM) disk. The magnetic disk mass storage device contains the read/write storage elements of the primary file system and encached read only storage elements from the WORM disk. Space is reserved on the unwritten portion of the WORM disk for the read-write storage elements of the primary file system. Techniques for performing file operations including opening, reading, writing, creating, and deleting files are disclosed, as well as techniques for performing the operations of dumping and restoring the primary file system.