TY  - CONF
AU  - Somorjai, Márk
AU  - Dobos-Kovács, Mihály
AU  - Bajczi, Levente
AU  - Ádám, Zsófia
AU  - Vörös, András
ED  - Kutsia, Temur
ED  - Ventura, Daniel
ED  - Monniaux, David
ED  - Morales, Jose F.
TI  - Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
T2  - Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
T3  - Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180 ; 402.
PY  - 2023
SP  - 105
EP  - 117
PG  - 13
DO  - 10.4204/EPTCS.402.11
UR  - https://m2.mtmt.hu/api/publication/33784283
ID  - 33784283
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Dobos-Kovács, Mihály
AU  - Vörös, András
ED  - Anon, A
TI  - Evaluation of SMT solvers in abstraction-based software model checking
T2  - Proceedings of the 11th Latin-American Symposium on Dependable Computing, LADC '22
PB  - Association for Computing Machinery (ACM)
CY  - New York, New York
SN  - 9781450397377
PY  - 2022
SP  - 109
EP  - 116
PG  - 8
DO  - 10.1145/3569902.3570187
UR  - https://m2.mtmt.hu/api/publication/33575796
ID  - 33575796
N1  - Export Date: 20 February 2023
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Szabó, Richárd
AU  - Vörös, András
ED  - Renczes, Balázs
TI  - Dependability Modeling of Cyber-Physical Systems in the Gamma Framework
T2  - Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics
PB  - BME Méréstechnika és Információs Rendszerek Tanszék
CY  - Budapest
SN  - 9789634218722
PY  - 2022
SP  - 20
EP  - 23
PG  - 4
UR  - https://m2.mtmt.hu/api/publication/32679018
ID  - 32679018
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Szabó, Richárd
AU  - Vörös, András
TI  - Towards formally analyzed Cyber-Physical Systems
T2  - Student Forum Proceedings- EDCC 2021
PB  - arXiv.org
CY  - München
PY  - 2021
SP  - 1
EP  - 4
PG  - 4
UR  - https://m2.mtmt.hu/api/publication/32678929
ID  - 32678929
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Dobos-Kovács, Mihály
AU  - Hajdu, Ákos
AU  - Vörös, András
ED  - Andrey, Brito
ED  - Fernando, Pedone
TI  - Bitvector Support in the Theta Formal Verification Framework
T2  - 2021 10th Latin-American Symposium on Dependable Computing (LADC)
PB  - IEEE
CY  - Piscataway (NJ)
SN  - 9781665478311
PY  - 2021
SP  - 01
EP  - 08
PG  - 8
DO  - 10.1109/LADC53747.2021.9672595
UR  - https://m2.mtmt.hu/api/publication/32678888
ID  - 32678888
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Nagy, Simon József
AU  - Szabó, Richárd
AU  - Vajda, Mate Levente
AU  - Vörös, András
ED  - Andrey, Brito
ED  - Fernando, Pedone
TI  - Demonstrator for dependable edge-based cyber-physical systems
T2  - 2021 10th Latin-American Symposium on Dependable Computing (LADC)
PB  - IEEE
CY  - Piscataway (NJ)
SN  - 9781665478311
PY  - 2021
SP  - 1
EP  - 8
PG  - 8
DO  - 10.1109/LADC53747.2021.9672569
UR  - https://m2.mtmt.hu/api/publication/32678847
ID  - 32678847
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Barcsa-Szabó, Áron
AU  - Várady, Balázs
AU  - Farkas, Rebeka
AU  - Molnár, Vince
AU  - Vörös, András
ED  - Renczes, Balázs
TI  - Towards Interactive Learning for Model-based Software Engineering
T2  - Proceedings of the 28th PhD Mini-Symposium
PB  - BME Méréstechnika és Információs Rendszerek Tanszék
CY  - Budapest
SN  - 9789634218456
PY  - 2021
SP  - 28
EP  - 31
PG  - 4
UR  - https://m2.mtmt.hu/api/publication/32527201
ID  - 32527201
AB  - Model-based technologies improve the efficiency of the design and development of IT systems by making it possible to automate verification, code generation and system analysis based on a formal model. A simple way of describing the behavior of systems is state-based modeling, which - due to the advancements of formal analysis techniques in recent years - can be widely and effectively utilized when analyzing systems. A possible way of synthesizing such models is to apply active automata learning algorithms. Acquiring a correct formal model of a system can be challenging because of the different theoretical and practical obstacles of both manual and automated approaches. We propose a semi-automated solution, that applies automata learning to provide an interactive environment for model development.
LA  - English
DB  - MTMT
ER  - 

TY  - CHAP
AU  - Csuvarszki, János Csanád
AU  - Graics, Bence
AU  - Vörös, András
ED  - Renczes, Balázs
TI  - Model-Driven Development of Heterogeneous Cyber-Physical Systems
T2  - Proceedings of the 28th PhD Mini-Symposium
PB  - BME Méréstechnika és Információs Rendszerek Tanszék
CY  - Budapest
SN  - 9789634218456
PY  - 2021
SP  - 24
EP  - 27
PG  - 4
UR  - https://m2.mtmt.hu/api/publication/31868691
ID  - 31868691
AB  - Cyber-physical systems (CPS) are becoming more prevalent for the reliable execution of critical tasks, e.g., in the aerospace and medical fields. The development of such systems is challenging, due to the heterogeneity of the components ranging from sensors and embedded controllers to cloud solutions. Model-driven approaches can provide a high-level abstraction to combat the challenges. This paper proposes a model-driven development approach supporting the precise modeling of CPS and the automatic derivation of implementation from the resulting models. The approach introduces a composition semantics tailored to heterogeneous architectures for the precise description of component interactions. Automated code generators allow the execution of standalone software components on real-time controllers and support the synthesis of standalone hardware components, enabling both the derivation of embedded software and the description of logical circuit behavior. Component interactions are supported by multiple communication solutions generally used in critical, real-time embedded systems. The approach is implemented in the Gamma framework and its applicability is demonstrated in two case studies.
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Nagy, Simon József
AU  - Graics, Bence
AU  - Marussy, Kristóf
AU  - Vörös, András
TI  - Simulation-based Safety Assessment of High-level Reliability Models
JF  - ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
J2  - ELECTRON PROC THEOR COMPUT SCI
VL  - 316
PY  - 2020
SP  - 240
EP  - 260
PG  - 21
SN  - 2075-2180
DO  - 10.4204/EPTCS.316.9
UR  - https://m2.mtmt.hu/api/publication/31374125
ID  - 31374125
AB  - Systems engineering approaches use high-level models to capture the architecture and behavior of the system. However, when safety engineers conduct safety and reliability analysis, they have to create formal models, such as fault-trees, according to the behavior described by the high-level engineering models and environmental/fault assumptions. Instead of creating low-level analysis models, our approach builds on engineering models in safety analysis by exploiting the simulation capabilities of recent probabilistic programming and simulation advancements. Thus, it could be applied in accordance with standards and best practices for the analysis of a critical automotive system as part of an industrial collaboration, while leveraging high-level block diagrams and statechart models created by engineers. We demonstrate the applicability of our approach in a case study adapted from the automotive system from the collaboration
LA  - English
DB  - MTMT
ER  - 

TY  - JOUR
AU  - Graics, Bence
AU  - Molnár, Vince
AU  - Vörös, András
AU  - Majzik, István
AU  - Varró, Dániel
TI  - Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems
JF  - SOFTWARE AND SYSTEMS MODELING
J2  - SOFTW SYST MODEL
VL  - 19
PY  - 2020
SP  - 1483
EP  - 1517
PG  - 35
SN  - 1619-1366
DO  - 10.1007/s10270-020-00806-5
UR  - https://m2.mtmt.hu/api/publication/31343505
ID  - 31343505
N1  - Deptartment of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary            
            MTA-BME Lendület Cyber-physical Systems Research Group, Budapest, Hungary            
            Department of Electrical and Computer Engineering, McGill University, Montreal, Canada            
            Cited By :6            
            Export Date: 9 June 2022            
            Correspondence Address: Graics, B.; MTA-BME Lendület Cyber-physical Systems Research GroupHungary; email: graics@mit.bme.hu
AB  - The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous, and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.
LA  - English
DB  - MTMT
ER  -