Modeling Distributed Real-Time Systems in TIOA and UPPAAL

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.


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...
Analysis of extended feature models with constraint programming
Karataş, Ahmet Serkan; Oğuztüzün, Mehmet Halit S.; Department of Computer Engineering (2010)
In this dissertation we lay the groundwork of automated analysis of extended feature models with constraint programming. Among different proposals, feature modeling has proven to be very effective for modeling and managing variability in Software Product Lines. However, industrial experiences showed that feature models often grow too large with hundreds of features and complex cross-tree relationships, which necessitates automated analysis support. To address this issue we present a mapping from extended fe...
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: