Show simple item record

Monitoring, testing, and abstractions of real -time specifications.

dc.contributor.authorBrockmeyer, Monica Anne
dc.contributor.advisorJahanian, Farnam
dc.date.accessioned2016-08-30T17:58:06Z
dc.date.available2016-08-30T17:58:06Z
dc.date.issued1999
dc.identifier.urihttp://gateway.proquest.com/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&res_dat=xri:pqm&rft_dat=xri:pqdiss:9959709
dc.identifier.urihttps://hdl.handle.net/2027.42/132080
dc.description.abstractAs real-time and safety-critical computer systems become more prevalent, increasing attention has been paid to the use of formal methods in the specification, validation, and verification of such systems. However, many techniques for analyzing and verifying real-time systems have not scaled well to real-life applications. This dissertation presents three analysis techniques which reduce the state-space and refine the portion of the state-space which is searched during specification analysis. These three techniques, <italic>selection, truncation, and abstraction</italic>, form the basis for a more focused examination of specification behavior. Monitoring modules describe a property that the system should satisfy. When they are used in the context of simulation, they provide a mechanism for evaluating properties of the system on a particular computation prefix. When used in the context of verification,<italic> reachability-based model-checking </italic> can be performed. This permits the generation of the state-space to be terminated upon satisfaction or violation of a property. Controller modules specify constraints which control which part of the state-space is to be examined by limiting the range of input events. When used in the context of simulation, they perform powerful steering of the simulation. When used in the context of verification, they permit verification of a subset of the state-space. MTSim is an extensible, customizable simulation platform for Modechart specifications, which supports examination of individual computation prefixes. Simulation-verification synthesizes simulation and verification to achieve an intermediate analysis method which is an application of the techniques of selection and truncation. This method uses simulation to limit generation of a computation graph to the set of computations consistent with the simulation. Abstraction relations between Modechart modules make it possible to determine when one specification <italic>implements</italic> another, i.e. when they have the same set of computations. Several abstraction relations are described and compared. A new representation of the semantics of a specification is introduced. This representation, <italic>min-max</italic> automata, is more compact than other types of finite state automata typically used to represent real-time systems, since each path can represent more than one computation. In addition, automatic generation of abstraction modules is described using a <italic>dependency marking</italic> approach.
dc.format.extent204 p.
dc.languageEnglish
dc.language.isoEN
dc.subjectAbstractions
dc.subjectFormal Verification
dc.subjectMonitoring
dc.subjectReal-time
dc.subjectSpecifications
dc.subjectTesting
dc.titleMonitoring, testing, and abstractions of real -time specifications.
dc.typeThesis
dc.description.thesisdegreenamePhDen_US
dc.description.thesisdegreedisciplineApplied Sciences
dc.description.thesisdegreedisciplineComputer science
dc.description.thesisdegreedisciplineSystems science
dc.description.thesisdegreegrantorUniversity of Michigan, Horace H. Rackham School of Graduate Studies
dc.description.bitstreamurlhttp://deepblue.lib.umich.edu/bitstream/2027.42/132080/2/9959709.pdf
dc.owningcollnameDissertations and Theses (Ph.D. and Master's)


Files in this item

Show simple item record

Remediation of Harmful Language

The University of Michigan Library aims to describe library materials in a way that respects the people and communities who create, use, and are represented in our collections. Report harmful or offensive language in catalog records, finding aids, or elsewhere in our collections anonymously through our metadata feedback form. More information at Remediation of Harmful Language.

Accessibility

If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.