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
  • 1
    Electronic Resource
    Electronic Resource
    Pragmatics of model checking: an STTT special section (1999)
    Springer
    International journal on software tools for technology transfer 2 (1999), S. 208-218 
    Details
    ISSN: 1433-2787
    Keywords: Key words: Model checking – Temporal logic – State explosion – System verification
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. Since its discovery in the early 1980s, model checking has emerged as one of the most exciting areas in the field of formal verification of system correctness. The chief reason for this enthusiasm resides in the fact that model checkers establish in a fully automated manner whether or not a system satisfies formal requirements; users need not construct proofs. Until the early 1990s, however, the practical impact of model checking was modest, in large part because the state-explosion problem limited the applicability of the technology. Recent advances in the field have dramatically expanded the scope of model checking, however, and interest in it on the part of practitioners is growing. This special section surveys several recent approaches to attacking the state explosion that are supporting the continued advancement of model checking as a viable technology for improved system design.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s100090050030
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    Generating diagnostic information for behavioral preorders (1995)
    Springer
    Distributed computing 9 (1995), S. 61-75 
    Details
    ISSN: 1432-0452
    Keywords: Key words: Formal methods ; Process algebra ; Verification algorithms ; Finite ; state systems
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Summary.  This paper describes a method for generating diagnostic information that explains why a given finite-state system fails to be greater than its specification with respect to the prebisimulation preorder. The information takes the form of a logical formula satisfied by the specification but not by the system and thus may be used by system designers for debugging purposes. Our technique relies on modifying an algorithm for computing the prebisimulation preorder so that information needed for generating these distinguishing formulas is saved appropriately. As a number of other behavioral preorders may be characterized in terms of prebisimulation preorder, our approach may be used as a basis for computing diagnostic information for these relations as well.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s004460050010
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    A linear-time model-checking algorithm for the alternation-free modal mu-calculus (1993)
    Springer
    Formal methods in system design 2 (1993), S. 121-147 
    Details
    ISSN: 1572-8102
    Keywords: Formal methods in system analysis ; automated verification ; model-checking algorithms
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We develop a model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in time proportional to the product of the sizes of the process and the formula; this improves on the best known algorithm for similar fixed-point logics.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01383878
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    Guest Editorial (1999)
    Springer
    Automated software engineering 6 (1999), S. 5-6 
    Details
    ISSN: 1573-7535
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1008606716885
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    Electronic Resource
    Electronic Resource
    A practical approach to implementing real-time semantics (1999)
    Springer
    Annals of software engineering 7 (1999), S. 127-155 
    Details
    ISSN: 1573-7489
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This paper investigates implementations of process algebras which are suitable for modeling concurrent real-time systems. It suggests an approach for efficiently implementing real-time semantics using dynamic priorities. For this purpose a process algebra with dynamic priority is defined, whose semantics corresponds one-to-one to traditional real-time semantics. The advantage of the dynamic-priority approach is that it drastically reduces the state-space sizes of the systems in question while preserving all properties of their functional and real-time behavior. The utility of the technique is demonstrated by a case study that deals with the formal modeling and verification of several aspects of the widely-used SCSI-2 bus-protocol. The case study is carried out in the Concurrency Workbench of North Carolina, an automated verification tool in which the process algebra with dynamic priority is implemented. It turns out that the state space of the bus-protocol model is about an order of magnitude smaller than the one resulting from real-time semantics. The accuracy of the model is proved by applying model checking for verifying several mandatory properties of the bus protocol.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1018982020561
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 6
    Electronic Resource
    Electronic Resource
    Type theory and concurrency (1988)
    Springer
    International journal of parallel programming 17 (1988), S. 153-206 
    Details
    ISSN: 1573-7640
    Keywords: Concurrency ; verification ; computer-aided reasoning ; semantics
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This paper describes the use of an automated reasoning tool, the Nuprl system, to formalize Milner's Calculus of Communicating Systems (CCS). The goals of this work are two-fold: the first is to investigate the feasibility of using systems like Nuprl to handle the formal detail arising from reasoning about concurrency, while the second is to develop a framework in which various formalisms for reasoning about concurrency may be presented in an automated fashion. To these ends, an implementation in Nuprl of a formal theory of concurrency is described, an implementation of CCS in this mechanized semantic theory presented, and two means of analyzing CCS terms are investigated.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01383954
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 7
    Electronic Resource
    Electronic Resource
    Tableau-based model checking in the propositional mu-calculus (1990)
    Springer
    Acta informatica 27 (1990), S. 725-747 
    Details
    ISSN: 1432-0525
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Summary This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00264284
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 8
    Electronic Resource
    Electronic Resource
    Testing equivalence as a bisimulation equivalence (1993)
    Springer
    Formal aspects of computing 5 (1993), S. 1-20 
    Details
    ISSN: 1433-299X
    Keywords: Process algebras ; Finite-state systems ; Behavioural preorders ; Automated verification
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract In this paper we show how the testing equivalences and preorders on transition systems may be interpreted as instances of generalized bisimulation equivalences and prebisimulation preorders. The characterization relies on defining transformations on the transition systems in such a way that the testing relations on the original systems correspond to (pre)bisimulation relations on the altered systems. On the basis of these results, it is possible to use algorithms for determining the (pre)bisimulation relations in the case of finite-state transition systems to compute the testing relations.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01211314
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 9
    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
  • 10
    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
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...