*banner
 

Reasoning about Timed Systems Using Boolean Methods
Sanjit A. Seshia, Randal Bryant, Kenneth Stevens

Citation
Sanjit A. Seshia, Randal Bryant, Kenneth Stevens. "Reasoning about Timed Systems Using Boolean Methods". Talk or presentation, 11, October, 2005.

Abstract
Timed systems are those whose correctness depends not only on their logical behavior, but also on the time at which they generate results. Examples include real-time operating systems and self-timed circuits. Models of such systems, such as timed automata, involve both Boolean state variables and real-valued variables measuring the passage of time. This talk presents a Boolean approach to modeling and verifying timed systems, with a focus on self-timed circuits. I will first discuss how circuits are modeled as timed automata where most timing assumptions are modeled using Boolean variables based on the notion of "generalized relative timing." Next, I will describe a purely Boolean approach to the fully symbolic model checking of timed automata, which is based on transformations to problems in the Boolean domain, such as Boolean satisfiability solving. The use of a Boolean approach in both modeling and verification enables reasoning about larger circuits than previous methods; among other results, our verifier found a potential error in a published self-timed circuit of a widely-used industrial microprocessor.

I will conclude with a description of related projects and directions for future work.

Electronic downloads

Citation formats  
  • HTML
    Sanjit A. Seshia, Randal Bryant, Kenneth Stevens. <a
    href="http://chess.eecs.berkeley.edu/pubs/3.html"
    ><i>Reasoning about Timed Systems Using Boolean
    Methods</i></a>, Talk or presentation,  11,
    October, 2005.
  • Plain text
    Sanjit A. Seshia, Randal Bryant, Kenneth Stevens.
    "Reasoning about Timed Systems Using Boolean
    Methods". Talk or presentation,  11, October, 2005.
  • BibTeX
    @presentation{SeshiaBryantStevens05_ReasoningAboutTimedSystemsUsingBooleanMethods,
        author = {Sanjit A. Seshia and Randal Bryant and Kenneth
                  Stevens},
        title = {Reasoning about Timed Systems Using Boolean Methods},
        day = {11},
        month = {October},
        year = {2005},
        abstract = {Timed systems are those whose correctness depends
                  not only on their logical behavior, but also on
                  the time at which they generate results. Examples
                  include real-time operating systems and self-timed
                  circuits. Models of such systems, such as timed
                  automata, involve both Boolean state variables and
                  real-valued variables measuring the passage of
                  time. This talk presents a Boolean approach to
                  modeling and verifying timed systems, with a focus
                  on self-timed circuits. I will first discuss how
                  circuits are modeled as timed automata where most
                  timing assumptions are modeled using Boolean
                  variables based on the notion of "generalized
                  relative timing." Next, I will describe a purely
                  Boolean approach to the fully symbolic model
                  checking of timed automata, which is based on
                  transformations to problems in the Boolean domain,
                  such as Boolean satisfiability solving. The use of
                  a Boolean approach in both modeling and
                  verification enables reasoning about larger
                  circuits than previous methods; among other
                  results, our verifier found a potential error in a
                  published self-timed circuit of a widely-used
                  industrial microprocessor. <p>I will conclude with
                  a description of related projects and directions
                  for future work.},
        URL = {http://chess.eecs.berkeley.edu/pubs/3.html}
    }
    

Posted by Mary Stewart on 12 Oct 2005.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

You are not logged in 
©2002-2014 Chess