ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • Concurrency workbench  (1)
  • Key words: Model checking – Modal mu-calculus – Protocol verification – State explosion – Real-time  (1)
  • 1
    Electronic Resource
    Electronic Resource
    Verification of an active control system using temporal process algebra (1996)
    Springer
    Engineering with computers 12 (1996), S. 46-61 
    Details
    ISSN: 1435-5663
    Keywords: Active structural control ; Calculus of communicating systems (CCS) ; Concurrency workbench ; Modechart ; Real-time systems ; Simulation ; Temporal CCS
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics , Technology
    Notes: Abstract In this paper we describe complementary approaches that can be used to ensure the reliability of real-time systems, such as those used in active structural control systems. These approaches include both model-checking and simulation, and are based on a temporal process algebra. We combine these formal methods with a high-level, graphical modeling technique, Modechart, to specify an active structural control system consisting of several processors. Timing requirements on the system are specified and verified with a combination of process algebraic models and modal logic, and various simulation concepts are described for debugging models and for gaining insight into system behavior.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01200261
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    Local model checking and protocol analysis (1999)
    Springer
    International journal on software tools for technology transfer 2 (1999), S. 219-241 
    Details
    ISSN: 1433-2787
    Keywords: Key words: Model checking – Modal mu-calculus – Protocol verification – State explosion – Real-time
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. This paper describes a local model-checking algorithm for the alternation-free fragment of the modal mu-calculus that has been implemented in the Concurrency Factory and discusses its application to the analysis of a real-time communications protocol. The protocol considered is RETHER, a software-based, real-time Ethernet protocol developed at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity Ethernet hardware. Our model-checking results show that (for a particular network configuration) RETHER makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller than the total amount that would result from a global analysis of the protocol. In the course of specifying and verifying RETHER, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design also possesses the properties of interest. This observation points out one of the often-overlooked benefits of formal verification: by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to uncover interesting design alternatives.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s100090050031
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...