Modeling Distributed Real-Time Systems in TIOA and UPPAAL

Date

2016-11-01

Author

Schmidt, Klaus Verner
Schmidt, Şenan Ece

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

137
views

0
downloads

The mission- and life-critical properties of distributed real-time systems require concurrent modeling, analysis, and formal verification in the design stage. The timed input/output automata (TIOA) framework and the UPPAAL software package are two widely used modeling and verification tools for this purpose. To this end, we develop the algorithm TUConvert for converting distributed TIOA models to UPPAAL behavioral models and formally prove its correctness. We demonstrate the applicability of our algorithm by the formal verification of a distributed real-time industrial communication protocol that is modeled by TIOA.

Subject Keywords

Hardware and Architecture, Software

URI

https://hdl.handle.net/11511/34445

Journal

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS

DOI

https://doi.org/10.1145/2964202

Collections

Department of Electrical and Electronics Engineering, Article

Suggestions

OpenMETU
Core

Performing and analyzing non-formal inspections of entity relationship diagram (ERD) ÇAĞILTAY, NERGİZ; TOKDEMİR, GÜL; Kilic, Ozkan; Topalli, Damla (Elsevier BV, 2013-08-01) Designing and understanding of diagrammatic representations is a critical issue for the success of software projects because diagrams in this field provide a collection of related information with various perceptual signs and they help software engineers to understand operational systems at different levels of information system development process. Entity relationship diagram (ERD) is one of the main diagrammatic representations of a conceptual data model that reflects users' data requirements in a databas...
A framework for reviewing domain specific conceptual models TANRIÖVER, ÖMER ÖZGÜR; Bilgen, Semih (Elsevier BV, 2011-09-01) Conceptual models are used in understanding and communicating the domain of interest during analysis phase of system development. As they are used in early phases, errors and omissions may propagate to later phases and may be very costly to correct. This paper proposes a framework for evaluating conceptual models when represented in a domain specific language based on UML constructs. The framework describes the main aspects to be considered when conceptual models are represented in a domain specific languag...
An Approach for introducing a set of domain specific components Yiğit, İbrahim Onuralp; Doğru, Ali Hikmet; Department of Computer Engineering (2015) In this thesis, a preliminary methodology is proposed for the determination of a set of components to populate the domain model of a Software Product Line infrastructure. Software Product Line based approaches focus on the reusability of assets for a family of software products. For effective reuse, the definition of reusable assets in this thesis considers variability in a domain. The approach is based on variability specifications that is rooted in Feature Models and is reflected to a component modeling n...
Synthesis of Monitoring Rules with STL Aydin, Sertac Kagan; Aydın Göl, Ebru (World Scientific Pub Co Pte Lt, 2020-09-01) Online monitoring is essential to enhance the reliability for various systems including cyber-physical systems and Web services. During online monitoring, the system traces are checked against monitoring rules in real time to detect deviations from normal behaviors. In general, the rules are defined as boundary conditions by the experts of the monitored system. This work studies the problem of synthesizing online monitoring rules in the form of temporal logic formulas in an automated way. The monitoring rul...
A process capability based assessment model for software workforce in emergent software organizations TANRIÖVER, ÖMER ÖZGÜR; Demirörs, Onur (Elsevier BV, 2015-01-01) Software process improvement frameworks for software organizations enable to identify opportunities for improving the processes as well as establishing road maps for improvement. However, software process improvement practice showed that to achieve a sustained, leveraged state, software organizations need to focus on the workforce as much as the process. Software process improvement frameworks address the people dimension indirectly through processes. To complement process assessment models/methods, there i...

Citation Formats

K. V. Schmidt and Ş. E. Schmidt, “Modeling Distributed Real-Time Systems in TIOA and UPPAAL,” ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, pp. 0–0, 2016, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/34445.