NDLI: A compositional proof system for an occam-like real-time language

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

A compositional proof system for an occam-like real-time language

Content Provider	Semantic Scholar
Author	Hooman, Jjm Jozef
Copyright Year	1987
Abstract	A compositional proof system is given for an Occam-like real-time programming language to specify and verify distributed synchronous message passing. Concurrency is modelled as "maximal parallelism"; that is, if a process can proceed it will do so immediately. A process only waits when no local action is possible and no partner is available for communication. Terminating arul non terminating processes can be specified from the viewpoint of an external observer with his own clock. This leads to a global notion of time. Furthermore we take a dense time domain. A speCification of a process consists of a Hoare triple (pre and post condition) extended with two invariants: an assumption about expected behaViour of the environment, and a commitment which is guaranteed by the process itself, as long as the environment satisfies the assumption. In deviation of earlier work [Hl, assumption and commitment may refer directly to the global time. This makes it possible to specify (and verify) that something must happen at a certain point of time. In the proof system emphasis is put on an easy way of reasoning at parallel composition. The parallel composition rule deals with checking and removing assumptions only. Maximal parallelism can be used locally by making SUitable assumptions and applying a separate "strengthen" rule which models the assumption/commitment reasoning. • supported by Esprit Project 937: Debugging and Specification of Ada Real-Time Embedded Systems (DESCARTES). Electronic-mail address: mcvax!eutrc3!wsinjh.UUCP (or wsdcjh@heithe5.BITNET).
File Format	PDF HTM / HTML
Volume Number	8714
Alternate Webpage(s)	https://pure.tue.nl/ws/files/2442201/8839479.pdf
Alternate Webpage(s)	http://alexandria.tue.nl/extra1/wskrap/publichtml/8839479.pdf
Language	English
Access Restriction	Open
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