Citation
Sanjit 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

• seshia11Oct05.ppt · application/vnd.ms-powerpoint · 2864 kbytes
• seshia11Oct05.pdf · application/pdf · 433 kbytes

• HTML

  Sanjit 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 Seshia, Randal Bryant, Kenneth Stevens.
  "Reasoning about Timed Systems Using Boolean
  Methods". Talk or presentation,  11, October, 2005.

• BibTeX

  @presentation{SeshiaBryantStevens05_ReasoningAboutTimedSystemsUsingBooleanMethods,
      author = {Sanjit 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.