1989 ◽  
Vol 3 (3) ◽  
pp. 335-340 ◽  
Author(s):  
Tapan K. Nayak

As the formal methods of proving correctness of a computer program are still very inadequate, in practice when a new piece of software is developed and all obvious errors are removed, it is tested with different (random) inputs in order to detect the remaining errors and assess its quality. We suppose that whenever the program fails the error causing the failure can be detected and removed correctly. Thus, the quality of the software increases as testing goes on. In this paper, we consider two different models and present the minimum variance unbiased estimators of the expected failure rate of the revised software at any time of testing t, based on the data generated up to that point.


Author(s):  
Radziah Mohamad ◽  
Dyg. Norhayati Abg. Jawawi ◽  
Safaai Deris ◽  
Rosbi Mamat

Aktiviti menguji sama ada sistem masa nyata memenuhi spesifikasi masa dan keserempakan adalah sangat penting. Salah satu bidang penyelidikan dalam bidang keboleh-percayaan perisian ialah teknik formal yang cuba untuk membuktikan kesahihan sesuatu atur cara dengan spesifikasinya. Oleh kerana masa dan keserampakan merupakan aspek yang penting dalam sistem masa nyata, keperluan untuk menggunakan teknik formal sebagai teknik untuk mengesahkan aspek masa dan keserempakan ini adalah amat tinggi. Kertas kerja ini mengkaji proses membina spesifikasi formal untuk sistem masa nyata berskala kecil dengan menggunakan teknik Z. Spesifikasi formal yang dibangunkan di dalam kertas kerja ini diharap dapat membantu proses penganalisisan fasa reka bentuk di awal proses pembangunan sistem. Kertas kerja ini juga diharap dapat menjadi rujukan kepada projek–projek teknik formal yang akan datang terutamanya projek yang berkaitan dengan sistem masa nyata berskala kecil. Kata kunci: Kebolehpercayaan perisian; spesifikasi formal; Z; masa nyata; sistem berskala kecil. 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 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. Key words: Software reliability; formal specification; Z; hard real-time; small-scale systems


1990 ◽  
Vol 5 (1) ◽  
pp. 2
Author(s):  
Barbara Kitchenham
Keyword(s):  

Sign in / Sign up

Export Citation Format

Share Document