Staff View
Modular Verification of Communicating Sequential Processes

Descriptive

Language
LanguageTerm (authority = ISO 639-3:2007); (type = text)
English
Genre (authority = RULIB-FS)
Other
Genre (authority = marcgt)
technical report
PhysicalDescription
InternetMediaType
application/pdf
Extent
37 p.
Note (type = special display note)
Technical report DCS-TR-150
Name (type = corporate); (authority = RutgersOrg-School)
NamePart
School of Arts and Sciences (SAS) (New Brunswick)
Name (type = corporate); (authority = RutgersOrg-Department)
NamePart
Computer Science (New Brunswick)
TypeOfResource
Text
TitleInfo
Title
Modular Verification of Communicating Sequential Processes
Abstract (type = abstract)
The semantics of communication in a distributed computing environment without shared objects are investigated from the viewpoint of modularity and hierarchical system structure. Communicating Sequential Processes (CSP), Hoare's language for parallel programming, is modified and expanded to support process modularity and hierarchical structure using a port construction. A formal axiomatic 'verification methodology for partial correctness is developed that extends the Hoare axiomatic proof methodology for sequential (nonparallel) programs to CSP-like programs, without resort to global invariants. Hierarchical structure and modularity are fully supported within the proof system. Processes are verified against an abstract entity, the interface, thereby achieving a formal notion of process specification and plug-compatibility. Alongside maintenance to a system is maintenance to its correctness proof, the two evolving side by side in an isomorphic fashion. The formalism is broadened further to include shared ports by the introduction of a universal assertion termed Kirchhoff's Law. Several examples are provided that demonstrate the methodology, including a modular proof of the generic single-entry, multiple-user CSP subroutine process.
Name (type = personal)
NamePart (type = family)
Akkoyunlu
NamePart (type = given)
E. A.
Affiliation
Brooklyn College
Role
RoleTerm (type = text); (authority = marcrt)
author
Name (type = personal)
NamePart (type = family)
Nemes
NamePart (type = given)
Richard M.
Affiliation
Computer Science (New Brunswick)
Role
RoleTerm (type = text); (authority = marcrt)
author
OriginInfo
DateCreated (encoding = w3cdtf); (qualifier = exact); (keyDate = yes)
1984-11
RelatedItem (type = host)
TitleInfo
Title
Computer Science (New Brunswick)
Identifier (type = local)
rucore21032500001
Location
PhysicalLocation (authority = marcorg); (displayLabel = Rutgers, The State University of New Jersey)
NjNbRU
Identifier (type = doi)
doi:10.7282/T33T9MP4
Back to the top

Rights

RightsDeclaration (AUTHORITY = rightsstatements.org); (TYPE = IN COPYRIGHT); (ID = http://rightsstatements.org/vocab/InC/1.0/)
This Item is protected by copyright and/or related rights.You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use.For other uses you need to obtain permission from the rights-holder(s).
Copyright
Status
Copyright protected
Availability
Status
Open
Reason
Permission or license
Back to the top

Technical

RULTechMD (ID = TECHNICAL1)
ContentModel
Document
Back to the top
Version 8.3.10
Rutgers University Libraries - Copyright ©2019