Stammdaten

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)
Art der Veröffentlichung Online Publikation
Erschienen in: 2018 International Conference on High Performance Computing & Simulation (HPCS)
2018 International Conference on High Performance Computing & Simulation (HPCS)
zur Publikation
 ( IEEE; )
Erscheinungdatum: 16.07.2018
Titel der Serie: -
Bandnummer: -
Erstveröffentlichung: Ja
Version: -
Seite: S. 642 - 649

Identifikatoren

ISBN: -
ISSN: -
DOI: http://dx.doi.org/10.1109/HPCS.2018.00106
AC-Nummer: -
Homepage: https://ieeexplore.ieee.org/abstract/document/8514411
Open Access
  • Online verfügbar (nicht Open Access)

Zuordnung

Organisation Adresse
Fakultät für Technische Wissenschaften
 
Institut für Informatik-Systeme
Universitätsstr. 65-67
A-9020  Klagenfurt
Österreich
  -993502
   sek-eder@isys.uni-klu.ac.at
https://www.aau.at/isys/
zur Organisation
Universitätsstr. 65-67
AT - A-9020  Klagenfurt

Kategorisierung

Sachgebiete
  • 101013 - Mathematische Logik
  • 101028 - Mathematische Modellierung
Forschungscluster Kein Forschungscluster ausgewählt
Peer Reviewed
  • Ja
Publikationsfokus
  • Science to Science (Qualitätsindikator: II)
Klassifikationsraster der zugeordneten Organisationseinheiten:
Arbeitsgruppen
  • Software Engineering Research Group

Kooperationen

Organisation Adresse
Università Politecnica delle Marche (UNIVPM)
P.zza Roma 22
60121  Ancona
Italien
P.zza Roma 22
IT - 60121  Ancona

Beiträge der Publikation

Keine verknüpften Publikationen vorhanden