Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system
The task of checking whether a real-time system satisfies its timing and concurrency specifications is extremely important. One major area of research addressing software reliability aspect is called formal method, which attempts to prove the correctness of programs with respect to system specificat...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Penerbit UTM Press
2001
|
| Subjects: | |
| Online Access: | http://eprints.utm.my/937/1/JT34D3.pdf |
| _version_ | 1825908994144731136 |
|---|---|
| author | Mohamad, Radziah Abang Jawawi, Dayang Norhayati Deris, Safaai Mamat, Rosbi |
| author_facet | Mohamad, Radziah Abang Jawawi, Dayang Norhayati Deris, Safaai Mamat, Rosbi |
| author_sort | Mohamad, Radziah |
| collection | ePrints |
| description | The task of checking whether a real-time system satisfies its timing and concurrency specifications is extremely important. One major area of research addressing software reliability aspect is called formal method, which attempts to prove the correctness of programs with respect to system specifications. Since, timing and concurrency properties can be very important in the operation of real-time systems, there is a need for applying formal methods to verify timing properties. This paper investigates the process of building a formal specification of a small-scale embedded hard real-time systems using Z. It is expected that the formal specification presented in this paper can provide assistance in analysing design trade-offs early in the development process. It is also expected that this paper can act as the foundation for any upcoming formal methods related project especially for small-scale real-time systems project. |
| first_indexed | 2024-03-05T17:55:32Z |
| format | Article |
| id | utm.eprints-937 |
| institution | Universiti Teknologi Malaysia - ePrints |
| language | English |
| last_indexed | 2024-03-05T17:55:32Z |
| publishDate | 2001 |
| publisher | Penerbit UTM Press |
| record_format | dspace |
| spelling | utm.eprints-9372017-11-01T04:17:51Z http://eprints.utm.my/937/ Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system Mohamad, Radziah Abang Jawawi, Dayang Norhayati Deris, Safaai Mamat, Rosbi T Technology (General) The task of checking whether a real-time system satisfies its timing and concurrency specifications is extremely important. One major area of research addressing software reliability aspect is called formal method, which attempts to prove the correctness of programs with respect to system specifications. Since, timing and concurrency properties can be very important in the operation of real-time systems, there is a need for applying formal methods to verify timing properties. This paper investigates the process of building a formal specification of a small-scale embedded hard real-time systems using Z. It is expected that the formal specification presented in this paper can provide assistance in analysing design trade-offs early in the development process. It is also expected that this paper can act as the foundation for any upcoming formal methods related project especially for small-scale real-time systems project. Penerbit UTM Press 2001-06 Article PeerReviewed application/pdf en http://eprints.utm.my/937/1/JT34D3.pdf Mohamad, Radziah and Abang Jawawi, Dayang Norhayati and Deris, Safaai and Mamat, Rosbi (2001) Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system. Jurnal Teknologi D (34D). pp. 25-40. ISSN 0127-9696 http://www.penerbit.utm.my/onlinejournal/34/D/JT34D3.pdf |
| spellingShingle | T Technology (General) Mohamad, Radziah Abang Jawawi, Dayang Norhayati Deris, Safaai Mamat, Rosbi Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system |
| title | Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system |
| title_full | Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system |
| title_fullStr | Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system |
| title_full_unstemmed | Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system |
| title_short | Formal specification of a wall-climbing robot using Z-A case study of small-scale embedded hard real-time system |
| title_sort | formal specification of a wall climbing robot using z a case study of small scale embedded hard real time system |
| topic | T Technology (General) |
| url | http://eprints.utm.my/937/1/JT34D3.pdf |
| work_keys_str_mv | AT mohamadradziah formalspecificationofawallclimbingrobotusingzacasestudyofsmallscaleembeddedhardrealtimesystem AT abangjawawidayangnorhayati formalspecificationofawallclimbingrobotusingzacasestudyofsmallscaleembeddedhardrealtimesystem AT derissafaai formalspecificationofawallclimbingrobotusingzacasestudyofsmallscaleembeddedhardrealtimesystem AT mamatrosbi formalspecificationofawallclimbingrobotusingzacasestudyofsmallscaleembeddedhardrealtimesystem |