Publication: Towards Model Checking Security of Real...
Master data
Title: | Towards Model Checking Security of Real Time Java Software |
Subtitle: | |
Abstract: | More and more software libraries and applications in high-performance computing and distributed systems are coded using the Java programming language. The correctness of such pieces of code w.r.t. a given set of security policies often depends on the correct handling of timing between concurrent or recurrent events. Model-checking has proven to be an effective tool for verifying correctness of software. In spite of the growing importance of this application area of formal methods, though, no one targets the problem of verifying the correctness of real-time software w.r.t. timed specifications. The few existing works focus on very different problems, such as schedulability analysis of Java tasks. We describe an approach combining rule-based static analysis together with symbolic execution of Java code to extract networks of timed automata from existing software and then use Uppaal to model-check it against timed specifications. We claim that this approach can be helpful in model-checking security policies of real time java software. |
Keywords: |
Publication type: | Article in Proceedings (Authorship) |
Publication date: | 16.07.2018 (Online) |
Published by: |
2018 International Conference on High Performance Computing & Simulation (HPCS)
2018 International Conference on High Performance Computing & Simulation (HPCS)
(
IEEE;
)
to publication |
Title of the series: | - |
Volume number: | - |
First publication: | Yes |
Version: | - |
Page: | pp. 642 - 649 |
Versionen
Keine Version vorhanden |
Publication date: | 16.07.2018 |
ISBN (e-book): | - |
eISSN: | - |
DOI: | http://dx.doi.org/10.1109/HPCS.2018.00106 |
Homepage: | https://ieeexplore.ieee.org/abstract/document/8514411 |
Open access |
|
Authors
Luca Spalazzi
|
||||
Francesco Spegni
|
||||
Giovanni Liva (internal) | ||||
Martin Pinzger (internal) |
Assignment
Organisation | Address | ||||
---|---|---|---|---|---|
Fakultät für Technische Wissenschaften
Institut für Informatik-Systeme
|
AT - A-9020 Klagenfurt |
Categorisation
Subject areas | |
Research Cluster | No research Research Cluster selected |
Peer reviewed |
|
Publication focus |
Classification raster of the assigned organisational units:
|
working groups |
|
Cooperations
Organisation | Address | ||
---|---|---|---|
Università Politecnica delle Marche (UNIVPM)
|
IT - 60121 Ancona |
Research activities
Projects: |
|
Publications: | No related publications |
Events: | No related events |
Lectures: | No related lectures |