×

TICC-paradigm to build formally verified parallel software for multi-core chips

  • US 7,979,844 B2
  • Filed: 05/05/2009
  • Issued: 07/12/2011
  • Est. Priority Date: 10/14/2008
  • Status: Expired due to Fees
First Claim
Patent Images

1. A method of building formally verified parallel software for multi-core chips using TICC™

  • -Paradigm, the term TICC™

    -Paradigm being used to refer to a collection of abstractions, each abstraction being simultaneously a programming abstraction and an abstraction of a component in parallel software systems, with associated methods of implementation, use and validation, said abstractions being embodied in a parallel program development and execution platform called TICC™

    -Ppde, all abstractions embodied together in TICC™

    -Ppde enabling the following;

    (i) specification of abstract designs for parallel software systems;

    designers of a parallel software system for an application Ap specifying the abstract design, Ap;

    design( ), for application Ap using abstractions, the term “

    abstract”

    being used to refer to specifications of intended computations in a manner not necessarily executable by a computer, but amenable for computers building a theory of intended computations using event classes, interactively validating the theory and reducing models specified by the theory to their final validated implementations of computer programs;

    (ii) event class theory of intended computations being called ALLowed Event Occurrence Patterns, ALLEOPs for short, the event class theory derived from Ap;

    design( ) being called Ap;

    ALLEOPS( ), Ap;

    ALLEOPS( ) specifying patterns of causal chains of event classes that may occur in the intended computations, requirements to be satisfied by Ap;

    design( ) being specified by designers in a Causal Temporal Logic (CTL) language, the set of CTL-assertions that specify requirements for Ap;

    design( ) being called Ap;

    requirements( ), computers using Ap;

    design( ), Ap;

    requirements( ) and Ap;

    ALLEOPS( ) to perform the following tasks;

    (a) TICC™

    -Ppde automatically deriving Ap;

    ALLEOPS( ) from Ap;

    design( ), TICC™

    -Ppde using Ap;

    ALLEOPS( ) to interactively formally validate all CTL-assertions in Ap;

    requirements( ) for the Ap;

    design( ), the term “

    formally validate”

    being used to refer to validations performed without having to execute in a computer any of the intended computations;

    (b) TICC™

    -Ppde assisting designers to reduce abstract Ap;

    design( ) to its validated implementation of computer programs through successive refinements, at each stage of refinement designers and implementers specifying intended computations in greater detail in a manner such that all formal validations done in all previous stages are preserved, at each stage of refinement designers updating Ap;

    requirements( ), TICCT™

    -Ppde automatically updating Ap;

    ALLEOPS( ), TICC™

    -Ppde assisting designers and implementers to formally interactively validate updated Ap;

    requirements( ), successive refinements, successive automatic theory updating and successive validations preserving all validations performed in all previous stages of refinements, this iterative refinement process ultimately yielding the complete validated implementation of executable computer programs for the parallel software system for application Ap, implementation at any stage of refinement being called Ap;

    implementation( ), Ap;

    implementation( ) satisfying all requirements in Ap;

    requirements( ) at every stage of refinement;

    (iii) automatically implement a Self-Monitoring System (SMS) for Ap;

    implementation( ) called Ap;

    SMS( ), Ap;

    SMS( ) monitoring Ap;

    implementation( ) while it is running, in parallel with its running, without interfering in any way with timings of computational events, instances of event classes specified in Ap;

    ALLEOPS( ) occurring while Ap;

    implementation( ) is running, Ap;

    SMS( ) using Ap;

    ALLEOPS( ) while monitoring Ap;

    implementation( ) to dynamically identify, report and take appropriate a priori defined actions, if errors are detected in event instance occurrences, while running Ap;

    implementation( ), or if pending errors are detected, or if a priori defined critical event instance patterns occur while Ap;

    implementation( ) is running, any departure of event instance occurrence patterns at run time from those specified for event classes in Ap;

    ALLEOPS( ) being construed as errors, any deviation of timings of event instances from those specified in Ap;

    ALLEOPS( ) being construed as a pending error, critical behaviors being defined by designers in terms of specific patterns of causal chains of event classes in Ap;

    ALLEOPS( ), Ap;

    SMS( ) providing the infrastructure for development of self-diagnosis, self-repair and learning capabilities for applications Ap;

    abstractions in TICC™

    -paradigm enabling TICC™

    -Ppde to provide above services being independent, it being possible to use each abstraction independently of other abstractions to build and run software systems, such software systems not providing all above services, in the following the phrase “

    programming abstraction”

    being used to refer to abstractions used in developing computer programs, the phrase “

    component abstraction”

    being used to refer to abstractions of components used in TICC™

    -Ppde parallel programs.

View all claims
  • 0 Assignments
Timeline View
Assignment View
    ×
    ×