NDLI: Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS

Please wait, while we are loading the content...

Volume 21, Issue 6, Nov. 1996

Volume 21, Issue 5, Sept. 1996

Volume 21, Issue 4, July 1996

Volume 21, Issue 3, May 1996

Test and analysis of software architectures

An efficient state space generation for analysis of real-time systems

An incremental approach to structural testing of concurrent software

Improving the accuracy of Petri net-based analysis of concurrent programs

Generating functional test cases in-the-large for time-critical systems from logic-based specifications

Structural specification-based testing with ADL

Issues in the full scale use of formal methods for automated testing

Experiences and lessons from the analysis of TCAS II

Predicting dependability by testing

Using perturbation analysis to measure variation in the information content of test sets

Linear and structural event sequence analysis

Separate computation of alias information for reuse

Critical slicing for software fault localization

The path-wise approach to data flow testing with pointer variables

Unconstrained duals and their use in achieving all-uses coverage

Software error analysis

Generation of multi-formalism state-space analysis tools

Beyond traditional program slicing

An approach to verification and validation of a reliable multicasting protocol

A semantic model of program faults

Towards a structural load testing tool

Automated test data generation for programs with procedures

Reachability analysis of feature interactions

Compositional verification by model checking for counter-examples

Elements of style

Constructing abstract models of concurrent real-time software

Using partial-order methods in the formal validation of industrial concurrent programs

Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS

A logic-model semantics for SCR software requirements

Why state-of-the-art is not state-of-the-practice (panel)

Volume 21, Issue 2, March 1996

Volume 21, Issue 1, Jan 1 1996

Formal specification and verification of the kernel functional unit of the OSI session layer protocol and service using CCS

Content Provider	ACM Digital Library
Author	Barjaktarovic, Milica Jabbour, Kamal Chin, Shiu-Kai
Abstract	This paper describes an application of formal methods to protocol specification, validation and verification. Formal methods can be incorporated in protocol design and testing so that time and resources are saved on implementation, testing, and documentation. In this paper we show how formal methods can be used to write the control sequence, i.e. pseudo code, which can be formally tested using automated support. The formal specification serves as a blueprint for a correct implementation with desired properties.As a formal method we chose a process algebra called "plain" Calculus of Communicating Systems (CCS). Our specific objectives were to: 1) build a CCS model of the Kernel Functional Unit of OSI session layer service: 2) obtain a session protocol specification through stepwise refinement of the service specification; and 3) verify that the protocol specification satisfies the service specification. We achieved all of our objectives. Verification and validation were accomplished by using the CCS's model checker, the Edinburgh Concurrency Workbench (CWB). We chose plain CCS because of itssuccinct, abstract, and modular specifications, strong mathematical foundation which allows for formal reasoning and proofs, and existence of the automated support tool which supports temporal logic. The motivation for this work is: 1) testing the limits of CCS's succinct notation; 2) combining CCS and temporal logic; and 3) using a model-checker on a real-life example.
Starting Page	270
Ending Page	279
Page Count	10
File Format	PDF
ISSN	01635948
DOI	10.1145/226295.226325
Journal	ACM SIGSOFT Software Engineering Notes (SOEN)
Volume Number	21
Issue Number	3
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1979-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in