Combining Extended UML Models and Formal Methods to Analyze Real-Time Systems

2005 ◽  
pp. 24-36 ◽  
Author(s):  
Nawal Addouche ◽  
Christian Antoine ◽  
Jacky Montmain
Keyword(s):  
Real Time ◽  
Formal Methods ◽  
Real Time Systems ◽  
Time Systems ◽  
Uml Models

Towards Early Verification of UML Models for Embedded and Real-Time Systems

2012 ◽  
Vol 45 (4) ◽  
pp. 25-30 ◽  
Author(s):  
Marco A. Wehrmeister ◽  
João G. Packer ◽  
Luis M. Ceron ◽  
Carlos E. Pereira
Keyword(s):  
Real Time ◽  
Real Time Systems ◽  
Time Systems ◽  
Uml Models

Specification and Validation of Real Time Systems

2011 ◽  
pp. 444-475
Author(s):  
Olfa Mosbahi
Keyword(s):  
Real Time ◽  
Formal Methods ◽  
Temporal Logic ◽  
Formal Method ◽  
The Other ◽  
Real Time Systems ◽  
Critical Systems ◽  
Temporal Properties ◽  
Integration Approach ◽  
Time Systems

The chapter presents a specification technique borrowing features from two classes of specification methods, formal and semi-formal ones. Each of the above methods have been proved to be useful in the development of real-time and critical systems and widely reported in different papers (Bruel, 1996; Clarke & Wing, 1996; Cohen, 1994; Fitzgerald & Larsen, 1994; Ghezzi, Mandrioli & Morzenti, 1990). Formal methods are based on mathematical notations and axiomatic which induce verification and validation. Semi-formal methods are, in the other hand, graphic, structural and uer-friendly. Each method is applied on a suitable case study, that we regret some missing features we could find in the other class. This remark has motivated our work. We are interested in the integration of formal and semi-formal methods in order to lay out a specification approach which combines the advantages of theses two classes of methods. The proposed technique is based on the integration of the semi-formal method STATEMATE (Harel, 1997; Harel, 1987) and the temporal logic FNLOG (Sowmya & Ramesh, 1997). This choice is justified by the fact that FNLOG is formal, deals with quantitative temporal properties and that these two approaches have a compatibility which simplifies their integration (Sowmya & Ramesh, 1997). The proposed integration approach uses the notations of STATEMATE and FNLOG, defines various transformation rules of a STATEMATE specification towards FNLOG and extends the axiomatics of the temporal logic FNLOG by new lemmas to deal with duration properties. The chapter presents the various steps of our integration approach, the proposed extentions and illustrates it over a case of critical real-time systems: the gas burner system (Ravn, Rishel & Hansen, 1993).

“Lean” formal methods in the development of provably correct real-time systems

1998 ◽  
Author(s):  
A. Cau ◽  
H. Zedan ◽  
B. Moszkowski ◽  
A. Ruddle
Keyword(s):  
Real Time ◽  
Formal Methods ◽  
Real Time Systems ◽  
Time Systems

Support for early verification of embedded real-time systems through UML models simulation

2012 ◽  
Vol 46 (1) ◽  
pp. 73-81 ◽  
Author(s):  
Marco A. Wehrmeister ◽  
Joao G. Packer ◽  
Luis M. Ceron
Keyword(s):  
Real Time ◽  
Real Time Systems ◽  
Time Systems ◽  
Uml Models

Formal Specification of a Wall-Climbing Robot Using Z – A Case Study of Small-Scale Embedded Hard Real-Time System

2012 ◽  
Author(s):  
Radziah Mohamad ◽  
Dyg. Norhayati Abg. Jawawi ◽  
Safaai Deris ◽  
Rosbi Mamat
Keyword(s):  
Real Time ◽  
Formal Methods ◽  
Software Reliability ◽  
Formal Specification ◽  
Small Scale ◽  
Real Time Systems ◽  
Time System ◽  
Real Time System ◽  
Hard Real Time ◽  
Time Systems

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

Sign in / Sign up

Export Citation Format

Share Document