ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

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
    Springer
    Requirements engineering 4 (1999), S. 188-197 
    ISSN: 1432-010X
    Keywords: Key words:Memory systems – Parallel applications – Predicate calculus
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Shared memory provides a convenient programming model for parallel applications. However, such a model is provided on physically distributed memory systems at the expense of efficiency of execution of the applications. For this reason, applications can give minimum consistency requirements on the memory system, thus allowing alternatives to the shared memory model to be used which exploit the underlying machine more efficiently. To be effective, these requirements need to be specified in a precise way and to be amenable to formal analysis. Most approaches to formally specifying consistency conditions on memory systems have been from the viewpoint of the machine rather than from the application domain.  In this paper we show how requirements on memory systems can be given from the viewpoint of the application domain formally in a first-order theory MemReq, to improve the requirements engineering process for such systems. We show the general use of MemReq in expressing major classes of requirements for memory systems and conduct a case study of the use of MemReq in a real-life parallel system out of which the formalism arose.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 2
    Electronic Resource
    Electronic Resource
    Springer
    Formal aspects of computing 8 (1996), S. 238-244 
    ISSN: 1433-299X
    Keywords: Calculus of communicating systems ; Parametric channels ; Parallel operating systems
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We present a concrete version of Astesiano and Zucca's CCS/PC, that permits parametric channels of a special form which are used in prefix expressions and in an extended way in relabelling functions. We report on the use of the calculus to describe nested process context in a parallel operating system.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 3
    Electronic Resource
    Electronic Resource
    Springer
    Software quality journal 8 (1999), S. 255-269 
    ISSN: 1573-1367
    Keywords: verification ; temporal logic ; high-level design ; operating systems
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The presence of an effective verification process at an earlier phase of the system development lifecycle will have a greater impact on productivity and product quality than a verification process at a later phase. The usual verification process at the later coding phases involves some form of testing. As high-level design cannot be tested in the same way as code, an option at that phase is some kind of formal verification. A process of verification is presented for the high-level design phase of an operating system development, where both rigorous and formal verification are used, and the rigorous directs the formal. The methodology is based on temporal logic. Formal proofs are manageable on an in-house theorem prover.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...