Distributed, Embedded and Intelligent Systems

  • Selma Lagerlöfs Vej 300, Cassiopeia

    9220 Aalborg

    Denmark

Research Output 1989 2020

2015
2 Citations (Scopus)

Decidability and Expressiveness of Recursive Weighted Logic

Xue, B., Larsen, K. G. & Mardare, R. I., 2015, Perspectives of Systems Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Voronkov, A. & Virbitskaite, I. (eds.). Springer, p. 216-231 (Lecture Notes in Computer Science; No. 8974).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Expressiveness
Decidability
Transition Systems
Logic
Multi-modal Logic

Fieldbook: Udvikling af embedded systemer & smarte produkter i praksis: Lav din virksomheds eget roadmap

Jensen, H. V., Agesen, M. K., Nyman, U. M. & Wolff, S., 10 Oct 2015, København V: Dansk industri. 80 p.

Research output: Book/ReportBookCommunication

Open Access
2 Citations (Scopus)
422 Downloads (Pure)

Flexible Framework for Statistical Schedulability Analysis of Probabilistic Sporadic Tasks

Boudjadar, J., Kim, J. H., David, A., Larsen, K. G., Mikucionis, M., Nyman, U., Skou, A., Lee, I. & Thi Xuan Phan, L., 2015, 18th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, ISORC 2015. IEEE, p. 74-83 (International Symposium on Object-Oriented Real-Time Distributed Computing).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

File
15 Citations (Scopus)

Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools

Kim, J. H., Larsen, K. G., Nielsen, B., Mikučionis, M. & Olsen, P., 2015, Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015 Oslo, Norway, June 22-23, 2015 Proceedings. Núñez, M. & Güdemann, M. (eds.). Springer, p. 47-61 (Lecture Notes in Computer Science; No. 9128).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2 Citations (Scopus)

Formal Methods for Modelling and Analysis of Single-Event Upsets

Hansen, R. R., Larsen, K. G., Olesen, M. C. & Wognsen, E. R., 2015, IEEE International Conference on Information Reuse and Integration (IRI 2015). IEEE, p. 287-294

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)

Formal synthesis of application and platform behaviors of embedded software systems

Kim, J. H., Kang, I., Choi, J-Y., Lee, I. & Kang, S., 2015, In : Software and Systems Modeling. 14, 2, p. 839-859

Research output: Contribution to journalJournal articleResearchpeer-review

Embedded Software
Embedded software
Application programs
Embedded Systems
Software System

Intermediate Joint Action Plan, D4.2

Adrians, G., De Colvenaer, M., Murillo, C., Nielsen, P. A., Nøhr, B., Skou, A. J., Urtiaga, C., Thiel, C. & Aaen, I., 30 Apr 2015

Research output: Book/ReportBookResearch

Open Access
20 Citations (Scopus)

Language Emptiness of Continuous-Time Parametric Timed Automata

Benes, N., Bezdek, P., Larsen, K. G. & Srba, J., 2015, Automata, Languages, and Programming: 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II. Halldórsson, M. M., Iwama, K., Kobayashi, N. & Speckmann, B. (eds.). Springer, p. 69-81 12 p. (Lecture Notes in Computer Science; No. 9135).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Clocks
Computability and decidability
Semantics
2 Citations (Scopus)

Linking spatial and dynamic models for traffic maneuvers

Olderog, E-R., Ravn, A. P. & Wisniewski, R., Dec 2015, 2015 54th Annual Conference on Decision and Control (CDC). IEEE, p. 6809-6816

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Measuring Cloud Service Health Using NetFlow/IPFIX: The WikiLeaks Case

Drago, I., Hofstede, R., Sadre, R., Sperotto, A. & Pras, A., 2015, In : Journal of Network and Systems Management. 23, 1, p. 58-88 31 p.

Research output: Contribution to journalJournal articleResearchpeer-review

HIgh speed networks
Outsourcing
Outages
Servers
Health
9 Citations (Scopus)

Modelling Socio-Technical Attacks with Timed Automata

David, N., David, A., Hansen, R. R., Larsen, K. G., Legay, A., Olesen, M. C. & Probst, C., 2015, Proceedings of the 7th ACM CCS International Workshop on Managing Insider Security Threats. Association for Computing Machinery, p. 21-28 7 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

10 Citations (Scopus)

On the Total Variation Distance of Semi-Markov Chains

Bacci, G., Bacci, G., Larsen, K. G. & Mardare, R. I., 2015, Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. Pitts, A. (ed.). Springer, Vol. 9034. p. 185-199 15 p. (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

Markov processes
Computability and decidability
Model checking
Computational complexity
Specifications
28 Downloads (Pure)

Parametric Verification of Weighted Systems

Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J. T., Larsen, K. G. & Mardare, R. I., 2015, In : Open Access Series in Informatics. 44, p. 77-90

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
File
Model checking
Linear equations
Linear systems
Mathematical operators
Semantics
5 Citations (Scopus)

Polynomial Time Decidability of Weighted Synchronization under Partial Observability

Kretínsky, J., Larsen, K. G., Laursen, S. & Srba, J., 2015, 26th International Conference on Concurrency Theory (CONCUR 2015). Aceto, L. & de Frutos Escrig, D. (eds.). Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 142-154 13 p. (Leibniz International Proceedings in Informatics, Vol. 42).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
Weighted Automata
Observability
Decidability
Polynomial time
Synchronization
4 Citations (Scopus)
380 Downloads (Pure)

Quantitative Schedulability Analysis of Continuous Probability Tasks in a Hierarchical Context

Kim, J. H., Boudjadar, J., Nyman, U., Mikucionis, M., Larsen, K. G., Skou, A., Lee, I. & Thi Xuan Phan, L., 4 May 2015, CBSE'15, Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering. Association for Computing Machinery, p. 91-100

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

File
12 Citations (Scopus)
269 Downloads (Pure)

Real-time specifications

David, A., Larsen, K. G., Legay, A., Nyman, U., Traonouez, L-M. & Wasowski, A., 2015, In : International Journal on Software Tools for Technology Transfer. 17, 1, p. 17-45 29 p.

Research output: Contribution to journalJournal articleResearchpeer-review

File
Specifications
Real time systems
Semantics
Chemical analysis
3 Citations (Scopus)

Refinement Checking on Parametric Modal Transition Systems

Benes, N., Kretínsky, J., Larsen, K. G., Møller, M. H., Sickert, S. & Srba, J., 2015, In : Acta Informatica. 52, 2, p. 269-297 31 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Syntactics
Computational complexity
Specifications
Experiments
3 Citations (Scopus)

Resource-Parameterized Timing Analysis of Real-Time Systems

Kim, J. H., Legay, A., Larsen, K. G., Mikučionis, M. & Nielsen, B., 2015, Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings. Piterman, N. (ed.). Springer, p. 190-205 (Lecture Notes in Computer Science; No. 9434).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

16 Citations (Scopus)

Safe and Optimal Adaptive Cruise Control

Larsen, K. G., Mikučionis, M. & Taankvist, J. H., 2015, Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday. Meyer, R., Platzer, A. & Wehrheim, H. (eds.). Springer, p. 260-277 18 p. (Lecture Notes in Computer Science; No. 9360).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

Adaptive cruise control
Controllers
9 Citations (Scopus)

Schedulability of Herschel revisited using statistical model checking

David, A., Larsen, K. G., Legay, A. & Mikučionis, M., 2015, In : International Journal on Software Tools for Technology Transfer. 17, 2, p. 187-199 13 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Model checking
Stop watches
Statistical Models
Satellites
Industry
3 Citations (Scopus)

Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics

Mateo, J. A., Srba, J. & Sørensen, M. G., 2015, In : Fundamenta Informaticae. 140, 1, p. 89-121 33 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Soundness
Work Flow
Continuous Time
Computability and decidability
Arc of a curve
6 Citations (Scopus)

Structural Operational Semantics for Continuous State Stochastic Transition Systems

Bacci, G. & Miculan, M., Aug 2015, In : Journal of Computer and System Sciences. 81, 5, p. 834–858

Research output: Contribution to journalJournal articleResearchpeer-review

Structural Operational Semantics
Transition Systems
Stochastic Systems
Semantics
Specifications
105 Downloads (Pure)

Studerendes oplevelse af reorganisering af problem-baseret læring på Aalborg Universitet

Dahl, B. & Hüttel, H., 2015, In : Dansk Universitetspaedagogisk Tidsskrift. 10, 19, p. 43-55

Research output: Contribution to journalJournal articleResearchpeer-review

Open Access
File
2 Citations (Scopus)
281 Downloads (Pure)

The Timed Decentralised Label Model

Pedersen, M. L., Sørensen, M. H., Lux, D., Nyman, U. M. & Hansen, R. R., 2015, Secure IT Systems: 20th Nordic Conference on Secure IT-Systems (NordSec 2015). Buchegger, S. & Dam, M. (eds.). Springer, p. 27-43 (Lecture Notes in Computer Science; No. 9417).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
8 Citations (Scopus)

To Do and Not To Do: Constrained Scenarios for Safe Smart House

Le Guilly, T., Smedegaard, J. H., Pedersen, T. & Skou, A. J., Jul 2015, International Conference on Intelligent Environments (IE), 2015. IEEE, p. 17-24 8 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Intelligent buildings
Graphical user interfaces
Large scale systems
Automation
156 Citations (Scopus)
573 Downloads (Pure)

Uppaal SMC tutorial

David, A., Larsen, K. G., Legay, A., Mikučionis, M. & Poulsen, D. B., 6 Jan 2015, In : International Journal on Software Tools for Technology Transfer. 17, 4, p. 397-415 19 p.

Research output: Contribution to journalJournal articleResearchpeer-review

File
Model checking
Semantics
46 Citations (Scopus)

Uppaal Stratego

David, A., Jensen, P. G., Larsen, K. G., Mikučionis, M. & Taankvist, J. H., 2015, Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015. Baier, C. & Tinelli, C. (eds.). London, UK: Springer, p. 206-211 6 p. (Lecture Notes in Computer Science; No. 9035).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Query languages
Model checking

Validating Timed Component Contracts

Le Guilly, T., Liu, S., Olsen, P., Ravn, A. P. & Skou, A. J., 2015, 41st Euromicro Conference on Software Engineering and Advanced Applications (SEAA), 2015. IEEE, p. 245-249

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Testing
Software testing
Synchronization
6 Citations (Scopus)
186 Downloads (Pure)

Widening the Schedulability Hierarchical Scheduling Systems

Boudjadar, J., David, A., Kim, J. H., Larsen, K. G., Mikučionis, M., Nyman, U. & Skou, A., 2015, Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers. Lanese, I. & Madelaine, E. (eds.). Springer, p. 209-227 18 p. (Lecture Notes in Computer Science; No. 8997).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
Scheduling
Model checking
Hierarchical systems
Statistical Models
2014
1 Citation (Scopus)

Adaptive Task Automata with Earliest-Deadline-First Scheduling

Hatvani, L., David, A., Seceleanu, C. & Pettersson, P., 2014, In : Electronic Communications of the EASST. 70, p. 1-15 15 p.

Research output: Contribution to journalConference article in JournalResearchpeer-review

Open Access
2 Citations (Scopus)

A decidable recursive logic forweighted transition systems

Larsen, K. G., Mardare, R. & Xue, B., 1 Jan 2014, Theoretical Aspects of Computing – ICTAC 2014 : 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings. Springer, Vol. 8687. p. 460-476 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Syntactics
Real time systems
Costs

A Decidable Recursive Logic for Weighted Transition Systems

Xue, B., Larsen, K. G. & Mardare, R. I., 2014, Theoretical Aspects of Computing – ICTAC 2014: 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings. Ciobanu, G. & Méry, D. (eds.). Springer Publishing Company, Vol. 8687. p. 460-476 17 p. (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Syntactics
Real time systems
Costs
5 Citations (Scopus)

Adequacy and Complete Axiomatization for Timed Modal Logic

Jaziri, S., Larsen, K. G., Mardare, R. I. & Xue, B., 2014, Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). Jacobs, B., Silva, A. & Staton, S. (eds.). Ithaca, New York: Elsevier, Vol. 308. p. 183-210 28 p. (Electronic Notes in Theoretical Computer Science, Vol. 308).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
3 Citations (Scopus)

A hybrid procedure for efficient link dimensioning

Schmidt, R. D. O., Sadre, R., Sperotto, A., Van Den Berg, H. & Pras, A., 4 Jul 2014, In : Computer Networks. 67, p. 252-269 18 p.

Research output: Contribution to journalJournal articleResearchpeer-review

A Metrized Duality Theorem for Markov Processes

Kozen, D., Mardare, R. I. & Panangaden, P., 2014, Electronic Notes in Theoretical Computer Science. 29 October 2014: Elsevier, Vol. 308. p. 211-227 17 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Duality Theorems
Markov Process
Pseudometric
Approximate Reasoning
Isometry
6 Citations (Scopus)
656 Downloads (Pure)

A modal specification theory for components with data

Bauer, S. S., Larsen, K. G., Legay, A., Nyman, U. & Wasowski, A., 1 Apr 2014, In : Science of Computer Programming. 83, p. 106–128 22 p.

Research output: Contribution to journalJournal articleResearchpeer-review

Open Access
File
Specifications
Chemical analysis
3 Citations (Scopus)

A real-time Java tool chain for resource constrained platforms

Korsholm, S. E., Søndergaard, H. & Ravn, A. P., 2014, In : Concurrency and Computation: Practice & Experience. 26, 14, p. 2407-2431

Research output: Contribution to journalJournal articleResearchpeer-review

16 Citations (Scopus)

Arrowhead Compliant Virtual Market of Energy

Ferreira, L. L., Siksnys, L., Pedersen, P., Stluka, P., Chrysoulas, C., Le Guilly, T., Albano, M., Skou, A., Teixeira, C. & Pedersen, T. B., Sep 2014, Emerging Technology and Factory Automation (ETFA), 2014 IEEE. IEEE, p. 1-8

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Industrial plants
Automation
Petrochemical plants
Joining
Refining

A safety-critical java technology compatibility kit

Søndergaard, H., Korsholm, S. E. & Ravn, A. P., Oct 2014, Proceedings of the 12th International Workshop on Java Technologies for Real-time and Embedded Systems . Association for Computing Machinery, p. 1-9

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2 Citations (Scopus)

Bad neighborhoods on the internet

Moura, G. C. M., Sadre, R. & Pras, A., Jul 2014, In : IEEE Communications Magazine. 52, 7, p. 132-139 8 p., 6852094.

Research output: Contribution to journalJournal articleResearchpeer-review

Internet
Internet service providers
Industry
Botnet
7 Citations (Scopus)

Battery-Aware Scheduling of Mixed Criticality Systems

Wognsen, E. R., Hansen, R. R. & Larsen, K. G., 2014, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications: 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II. Margaria, T. & Steffen, B. (eds.). Springer Publishing Company, Vol. 8803. p. 208-222 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)

Bisimulation on Markov Processes over Arbitrary Measurable Spaces

Bacci, G., Bacci, G., Larsen, K. G. & Mardare, R. I., 2014, Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday. van Breugel, F., Kashefi, E., Palamidessi, C. & Rutten, J. (eds.). Springer Publishing Company, Vol. 8464. p. 76-95 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Measurable space
Bisimulation
Markov Process
Arbitrary
Adjunction
1 Citation (Scopus)

Certifiable Java for Embedded Systems

Schoeberl, M., Dalsgaard, A. E., Hansen, R. R., Korsholm, S. E., Ravn, A. P., Rivas, J. R. R., Strøm, T. B. & Søndergaard, H., 2014, Proceedings of the 12th International Workshop on Java Technologies for Real-time and Embedded Systems. Association for Computing Machinery, p. 10-19 10 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

2 Citations (Scopus)
476 Downloads (Pure)

Coccinelle: Tool support for automated CERT C Secure Coding Standard certification

Olesen, M. C., Hansen, R. R., Lawall, J. L. & Palix, N. J-M., Oct 2014, In : Science of Computer Programming. 91, Part B, p. 141-160

Research output: Contribution to journalConference article in JournalResearchpeer-review

File
7 Citations (Scopus)

Complete proof systems for weighted modal logic

Larsen, K. G. & Mardare, R., 21 Aug 2014, In : Theoretical Computer Science. 546, p. 164-175

Research output: Contribution to journalJournal articleResearchpeer-review

Proof System
Modal Logic
Labels
Theorem proving
Model checking
6 Citations (Scopus)
259 Downloads (Pure)

Compositional Schedulability Analysis of An Avionics System Using UPPAAL

Boudjadar, J., Larsen, K. G., Kim, J. H. & Nyman, U., 2014, Proceedings of the 1st International Conference on Advanced Aspects of Software Engineering, {ICAASE} 2014, Constantine, Algeria, November 2-4, 2014. CEUR Workshop Proceedings, Vol. 1294. p. 140-147 8 p.

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
4 Citations (Scopus)

Continuity Properties of Distances for Markov Processes

Jaeger, M., Mao, H., Larsen, K. G. & Mardare, R. I., 2014, Quantitative Evaluation of Systems: 11th International Conference, QEST 2014, Florence, Italy, September 8-10, 2014. Proceedings. Norman, G. & Sanders, W. (eds.). Springer, Vol. 8657. p. 297-312 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Distance Function
Markov Process
Kullback-Leibler Distance
Trace
Metric

Convergence to the European Energy Policy in European countries: case studies and comparison

Teixeira, C., Albano, M., Skou, A., Dueñas, L. P., Antonacci, F., Ferreira, R., Pedersen, K. L. & Scalari, S., 2014, In : Journal of Social Technologies. 4, 1, p. 7-24

Research output: Contribution to journalJournal articleResearchpeer-review

Open Access
Energy policy
Energy management
Smart meters
Environmental technology
Free energy
8 Citations (Scopus)
342 Downloads (Pure)

Degree of Schedulability of Mixed-Criticality Real-time Systems with Probabilistic Sporadic Tasks

Boudjadar, J., David, A., Kim, J. H., Larsen, K. G., Nyman, U., Skou, A. & Mikučionis, M., 1 Sep 2014, Theoretical Aspects of Software Engineering Conference (TASE), 2014. IEEE Computer Society Press, p. 126-130 5 p. (TASE).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Open Access
File
Real time systems
Probability distributions
Scheduling
Model checking
Quality of service
4 Citations (Scopus)

Efficient Controller Synthesis for a Fragment of MTL(0,∞)

Bulychev, P., David, A., Larsen, K. G. & Li, G., 1 Jan 2014, In : Acta Informatica. 51, 3-4, p. 165-192 28 p.

Research output: Contribution to journalJournal articleResearchpeer-review