Publikation: Towards Model Checking Security of Real...
Stammdaten
Titel: | Towards Model Checking Security of Real Time Java Software |
Untertitel: | |
Kurzfassung: | 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. |
Schlagworte: |
Publikationstyp: | Beitrag in Proceedings (Autorenschaft) |
Erscheinungsdatum: | 16.07.2018 (Online) |
Erschienen in: |
2018 International Conference on High Performance Computing & Simulation (HPCS)
2018 International Conference on High Performance Computing & Simulation (HPCS)
(
IEEE;
)
zur Publikation |
Titel der Serie: | - |
Bandnummer: | - |
Erstveröffentlichung: | Ja |
Version: | - |
Seite: | S. 642 - 649 |
Versionen
Keine Version vorhanden |
Erscheinungsdatum: | 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 |
|
AutorInnen
Luca Spalazzi
|
||||
Francesco Spegni
|
||||
Giovanni Liva (intern) | ||||
Martin Pinzger (intern) |
Zuordnung
Organisation | Adresse | ||||
---|---|---|---|---|---|
Fakultät für Technische Wissenschaften
Institut für Informatik-Systeme
|
AT - A-9020 Klagenfurt |
Kategorisierung
Sachgebiete | |
Forschungscluster | Kein Forschungscluster ausgewählt |
Peer Reviewed |
|
Publikationsfokus |
Klassifikationsraster der zugeordneten Organisationseinheiten:
|
Arbeitsgruppen |
|
Kooperationen
Organisation | Adresse | ||
---|---|---|---|
Università Politecnica delle Marche (UNIVPM)
|
IT - 60121 Ancona |
Forschungsaktivitäten
(Achtung: Externe Aktivitäten werden im Suchergebnis nicht mitangezeigt)
Projekte: |
|
Publikationen: | Keine verknüpften Publikationen vorhanden |
Veranstaltungen: | Keine verknüpften Veranstaltung vorhanden |
Vorträge: | Keine verknüpften Vorträge vorhanden |