WEKO3
Item
Formalization of Mutual Exclusion Algorithms in N-labeled Calculus
https://aist.repo.nii.ac.jp/records/2001762
https://aist.repo.nii.ac.jp/records/200176261bb3784-b798-4086-8762-5149b2440ae1
| Item type | Research Data (v9)(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| PubDate | 2014-01-01 | |||||||||
| Data name | ||||||||||
| Title | Formalization of Mutual Exclusion Algorithms in N-labeled Calculus | |||||||||
| Language | en | |||||||||
| Description of data | ||||||||||
| Description Type | Abstract | |||||||||
| Description | A family of formal systems called "labeled calculi" have been investigated lately for verification and analysis of timeconcerned cooperating program systems. These calculi have high formality since they are based on the Peano arithmetic, one of the natural number theories. They are axiom- and proof-based approaches, i.e. properties of systems are verified by formal proofs. These approaches are more rigid and precise than that of modelchecking. Among the labeled calculi, N-labeled calculus is the simplest and suited for usual time-concerned programs such as mutual exclusion. Mutual exclusion algorithms are indispensable for contemporary programs having parallel tasks/jobs/processes, and they offer typical examples of verification of such time-concerned cooperating programs. In this article, two mutual exclusion algorithms are formally represented in the calculus for verification. | |||||||||
| Language | en | |||||||||
| Author (Creator) name |
水谷哲也
× 水谷哲也
× 富田 康治
|
|||||||||
| Access Rights | ||||||||||
| Access Rights | open access | |||||||||
| Access Rights URI | http://purl.org/coar/access_right/c_abf2 | |||||||||
| APC | ||||||||||
| APC | Not required | |||||||||
| Rights Holder | ||||||||||
| Right Holder Name | 水谷哲也 | |||||||||
| Language | en | |||||||||
| Publisher | ||||||||||
| Publisher | IEEE | |||||||||
| Language | en | |||||||||
| Date | ||||||||||
| Date | 2014-01-01 | |||||||||
| Date Type | Issued | |||||||||
| Language | ||||||||||
| Language | eng | |||||||||
| Resource Type | ||||||||||
| Resource Type Identifier | http://purl.org/coar/resource_type/c_6501 | |||||||||
| Resource Type | journal article | |||||||||
| Identifier | ||||||||||
| Identifier | 10.1109/ITAIC.2014.7065010 | |||||||||
| Identifier Type | DOI | |||||||||
| Relation | ||||||||||
| Relation Type | isVersionOf | |||||||||
| Identifier Type | URI | |||||||||
| Related Identifier | http://ieeexplore.ieee.org/document/7065010/ | |||||||||
| Language | ja | |||||||||
| Related Title | 関連 URI | |||||||||
| Source Title | ||||||||||
| Source Title | Proceedings of the 2014 IEEE 7th Joint International Information Technology and Artificial Intelligence Conference (ITAIC 2014) | |||||||||
| Language | en | |||||||||
| Page Start | ||||||||||
| Start Page | 83 | |||||||||
| Page End | ||||||||||
| End Page | 88 | |||||||||
