mdh.sePublikationer
Ändra sökning
Avgränsa sökresultatet
123 1 - 50 av 112
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Träffar per sida
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
Markera
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Asplund, Lars
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Johnson, B.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Burns, Alan
    Session Summary: The Ravenscar Profile and Implementation Issues1999Ingår i: ACM SIGAda Ada Letters, Vol. XIX, nr 2, s. 12-14Artikel i tidskrift (Övrigt vetenskapligt)
  • 2.
    Asplund, Lars
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Safety Critical Systems Based on Formal Models2000Ingår i: ACM SIGAda Letters, ISSN 1094-3641, Vol. XX, nr 4, s. 32-39Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The Ravenscar profile for high integrity systems using Ada 95 is well defined in all real-time aspects. The complexity of the run-time system has been reduced to allow full utilization of formal methods for applications using the Ravenscar profile. In the Mana project a tool set is being developed including a formal model of a Ravenscar compliant run-time system, a gnat compatible run-time system, and an ASIS based tool to allow for the verification of a system including both COTS and code that is reused.

  • 3.
    Asplund, Lars
    et al.
    Uppsala University, Sweden.
    Lundqvist, Kristina
    Massachusetts Institute of Technology, USA.
    Safety Critical Systems Based on Formal Models2000Ingår i: ACM SIGAda Ada Letters - special issue on presentations from SIGAda 2000, Vol. XX, Iss. 4, 2000Konferensbidrag (Övrigt vetenskapligt)
  • 4.
    Asplund, Lars
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    MIT, Cambridge, MA, United States .
    The Gurkh Project: A Framework for Verification and Execution of Mission Critical Applications2003Ingår i: AIAA/IEEE Digital Avionics Systems Conference - Proceedings, vol. 2, 2003, s. 10.B.1/1-10.B.1/9Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    The paper contributes with three methods that together will make a complete tool-set for verification of mission critical applications. The first method is the transformation of existing Ada or VHDL code into an intermediate form. This form is used for verification by numerous different model checkers. The second method is a predictable runtime kernel that has both a verifiable formal model and is implemented in hardware to achieve full predictability. Finally, a method for transforming the intermediate form of the complete system into a hardware unit, the SafetyChip that performs runtime control of the system. This SafetyChip can catch 'out-of-state' behaviors.

  • 5.
    Berglund, Anders
    et al.
    Uppsala University, Sweden.
    Daniels, Mats
    Uppsala University, Sweden.
    Lundqvist, Kristina
    Uppsala University, Sweden.
    Westlund, Elvy
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Encouraging Active Participation in Programming Classes1996Ingår i: Selected papers from the 7th national conference on college teaching and learning, 1996Konferensbidrag (Övrigt vetenskapligt)
  • 6.
    Björnander, Stefan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Grunske, Lars
    Faculty of ICT, Swinburne University of Technology, Hawthorn VIC 3122, Australia.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Timed Simulation of Extended AADL-Based Architecture Specifications with Timed Abstract State Machines2009Ingår i: Architectures for Adaptive Software Systems: 5th International Conference on the Quality of Software Architectures, QoSA 2009, East Stroudsburg, PA, USA, June 24-26, 2009 Proceedings, Berlin: Springer, 2009, s. 101-115Kapitel i bok, del av antologi (Refereegranskat)
    Abstract [en]

    The Architecture Analysis and Design Language (AADL) is a popular language for architectural modeling and analysis of software intensive systems in application domains such as automotive, avionics, railway and medical systems. These systems often have stringent real-time requirements. This paper presents an extension to AADL's behavior model using time annotations in order to improve the evaluation of timing properties in AADL. The translational semantics of this extension is based on mappings to the Timed Abstract State Machines (TASM) language. As a result, timing analysis with timed simulation or timed model checking is possible. The translation is supported by art Eclipse-based plug-in and the approach is validated with a case study of an industrial production cell system.

    Ladda ner fulltext (pdf)
    fulltext
  • 7.
    Björnander, Stefan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Land, Rikard
    System Safety CrossControl AB.
    Graydon, Patrick
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Conmy, Philippa
    University of York.
    A method to formally evaluate safety case arguments against a system architecture model2012Ingår i: Proceedings of International Symposium on Software Reliability Engineering Workshops, ISSREW, 2012, s. 337-342Konferensbidrag (Refereegranskat)
    Abstract [en]

    For a large and complex safety-critical system, where safety is ensured by a strict control over many properties, the safety information is structured into a safety case. As a small change to the system design may potentially affect a large section of the safety argumentation, a systematic method for evaluating the impact of system changes on the safety argumentation would be valuable. We have chosen two of the most common notations: the Goal Structuring Notation (GSN) for the safety argumentation and the Architecture Analysis and Design Language (AADL) for the system architecture model. In this paper, we address the problem of impact analysis by introducing the GSN and AADL Graph Evaluation (GAGE) method that maps safety argumentation structure against system architecture, which is also a prerequisite for successful composition of modular safety cases. In order to validate the method, we have implemented the GAGE tool that supports the mapping between the GSN and AADL notations and highlight changes in impact on the argumentation. © 2012 IEEE.

  • 8.
    Björnander, Stefan
    et al.
    CrossControl AB.
    Seceleanu, Cristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    A Formal Analysis Framework for AADL2011Ingår i: The Journal of Science and Technology, ISSN 0866-708X, Vol. 49, nr 5Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    As system failure of mission-critical embedded systems may result in serious consequences, the development process should include verification techniques already at the architectural design stage, in order to provide evidence that the architecture fulfils its requirements. The Architecture Analysis and Design Language (AADL) is a language designed for modeling embedded systems, and its Behavior Annex defines the behavior of the system. However, even though it is an internationally used industry standard, AADL still lacks a formal semantics and is not executable, which limits the possibility to perform formal verification. In this paper, we introduce a formal analysis framework for a subset of AADL and its Behavior Annex, which includes the following: a denotational semantics, its implementation in Standard ML, and a graphical Eclipse-based tool encapsulating the implementation. We also show how to perform model checking of AADL properties defined in the Computation Tree Logic (CTL).

  • 9.
    Björnander, Stefan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Seceleanu, Cristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    ABV: A Verifier for the Architecture Analysis and Description Language (AADL)2011Ingår i: 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2011, 2011, s. 355-360Konferensbidrag (Refereegranskat)
    Ladda ner fulltext (pdf)
    fulltext
  • 10.
    Björnander, Stefan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Seceleanu, Cristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    The Architecture Analysis and Design Language and the Behavior Annex: A Denotational Semantics2011Rapport (Övrigt vetenskapligt)
    Abstract [en]

    We present a denotational semantics for the Architecture Analysis and Design Language with Behavior Annex and the Computational Tree logic. We also present tool support as an OSATE plug-in as well as the Production Cell case study.

  • 11.
    Björnfot, Lars
    et al.
    Uppsala University, Sweden.
    Asplund, Lars
    Uppsala University, Sweden.
    Lundqvist, Kristina
    Uppsala University, Sweden.
    Wall, Göran
    Uppsala University, Sweden.
    Distributed Run-Time System, a Protocol for Ada1993Ingår i: Proc. Ada-Europe'93, LNCS 688, 1993, s. 249-263Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    The requirements and specification of a protocol for low level communication between the run-time systems in a distributed Ada environment is presented. This allows an Ada system to be separated into software resources and run-time controllers. Calls to the local run-time system of a node, concerning task management, are transformed into remote calls to the controller, that schedules all tasks in the application. The calls to the run-time system together with all messages, requests and replies, that are triggered as a consequence, are described. The controller will be implemented in hardware separate from the processors. Communication between processors and controllers are by means of high speed (Gigabit) networks. In the proposed system, partitioning and distribution of Ada programs can fully utilize the inherent and strong type checking in Ada.

  • 12.
    Björnfot, Lars
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Uppsala University, Uppsala, Sweden.
    Wall, Göran
    Uppsala University, Uppsala, Sweden.
    Asplund, Lars
    Uppsala University, Uppsala, Sweden.
    Distribution of Tasks Within a Centrally Scheduled Local Area Network1994Ingår i: Proc. Ada-Europe'94, LNCS 887, 1994, s. 421-432Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    Distribution of a single Ada program on a local area network is accomplished by partitioning the run-time system into two parts. A central scheduling module is responsible for task management. Distributed run-time executives handle context switches and remote entry calls; however all activities are supervised by the scheduler. The scheduler can be implemented in hardware in order to achieve high efficiency. A network based on optical fibers is necessary due to the high speed required for system calls. Asynchronous Transfer Mode is suggested as the protocol for the communication. We describe an implementation of the divided run-time system on an Ethernet network, using MC68030-based micro computers as targets and an Ada program executing on a Rational host as the scheduler.

  • 13.
    Björnfot, Lars
    et al.
    Uppsala University, Sweden.
    Lundqvist, Kristina
    Uppsala University, Sweden.
    Wall, Göran
    Uppsala University, Sweden.
    Asplund, Lars
    Uppsala University, Sweden.
    Termination of Ada Tasks in Hardware1995Ingår i: Proc. TRI-Ada'95, 1995, s. 474-486Konferensbidrag (Övrigt vetenskapligt)
  • 14. Boussemart, Yves
    et al.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    The Gurkh Framework: an Industrial Case Study and Certification Issues for Safety Critical Software2006Konferensbidrag (Övrigt vetenskapligt)
  • 15.
    Boussemart, Yves
    et al.
    Massachusetts Institute of Technology, USA.
    Ouimet, Martin
    Massachusetts Institute of Technology, USA.
    Gorelov, Sebastien
    Massachusetts Institute of Technology, USA.
    Lundqvist, Kristina
    Massachusetts Institute of Technology, USA.
    Non-Intrusive System-Level Fault Tolerance for an Electronic Throttle Controller2006Ingår i: Proceedings ICN 2006, ICONS 2006, MVL 2006, 2006Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper describes the methodology used to add nonintrusive system-level fault tolerance to an electronic throttle controller. The original model of the throttle controller is a hybrid system created at a major automotive company. We use Gurkh as a framework within which we translate the hybrid model into a set of timed automata and perform analysis using formal methods. The first step of the translation process is to transform the hybrid model and its static schedule into Gurkh’s preemptive tasking paradigm. Using the UPPAAL tool, we then check the correctness of the resulting set of timed-automata by formally verifying reachability and timing properties. We also propose a method for quantifying the quality of the translation by estimating the amount of jitter thence introduced. The final step is the implementation of a Monitoring Chip based on the formal system model. The chip provides non-intrusive "out-of-path" and timing error detection which in turn allows for fault tolerance at a system level.

  • 16.
    Causevic, Aida
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Fotouhi, Hossein
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Data Security and Privacy in Cyber-Physical Systems for Healthcare2017Ingår i: Security and Privacy in Cyber-Physical Systems: Foundations, Principles, and Applications / [ed] Houbing Song D, Glenn A. Fink PhD, and Sabina Jeschke Dr. rer. nat., Wiley-IEEE Press , 2017, s. 305-320Kapitel i bok, del av antologi (Övrigt vetenskapligt)
  • 17.
    Dardar, Raghad
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Gallina, Barbara
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Johnsen, Andreas
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Nyberg, Mattias
    Scania AB, Södertälje, Sweden.
    Industrial Experiences of Building a Safety Case in Compliance with ISO 262622012Ingår i: 23RD IEEE INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING WORKSHOPS (ISSREW 2012), 2012, s. 349-354Konferensbidrag (Refereegranskat)
    Abstract [en]

    The ISO 26262 functional safety standard provides appropriate development processes, requirements and safety integrity levels specific for the automotive domain. One crucial requirement consists of the creation of a safety case, a structured argument, which inter-relates evidence and claims, needed to show that safety-critical systems are acceptably safe. The standard is currently not mandatory to be applied to safety critical systems installed in heavy trucks; however, this is likely to be changed by 2016. This paper describes the experience gathered by applying the standard to the Fuel Level Estimation and Display System, a subsystem that together with other subsystems plays a significant role in terms of global system safety for heavy trucks manufactured by Scania. More specifically, exploratory and laborious work related to the creation of a safety case in compliance with ISO 26262 in an inexperienced industrial setting is described, and the paper ends with presenting some lessons learned together with guidelines to facilitate the adoption of ISO 26262.

  • 18.
    Forsberg, Håkan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Ekstrand, Fredrik
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Otterskog, Magnus
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Early Results and Ideas for Enhancements of the Master of Engineering Programme in Dependable Aerospace Systems2017Ingår i: The 6th Development Conference for Swedish Engineering USIU2017, 2017Konferensbidrag (Refereegranskat)
    Abstract [en]

    The five-year Master of Engineering Programme in Dependable Aerospace Systems, with dependability as its silver thread, started at Mälardalen University (MDH) in 2015. This paper presents selected ideas behind the creation of the programme, together with some preliminary analysis of current results and suggested enhancements for the programme’s fourth and fifth years.

  • 19.
    Forsberg, Håkan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Forsberg, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Methods for Enhancement of a Master of Engineering Programme2019Konferensbidrag (Refereegranskat)
    Abstract [en]

    This paper describes methods we used to improve our Master of Engineering programme in Dependable Aerospace Systems together with the industry. The target audience is mainly programme coordinators/managers who are in the process to develop their programmes for future demands. The two main questions we address are: Q1 – How do we ensure a good progression within a programme to ensure the industry’s current and future needs in engineering skills? and Q2 – How do we ensure students become acquainted with research during their studies? The results indicate that our suggested method to analyse programme progression through subject abilities supports developer of engineering programmes and that our approach to undergraduate research opportunities is a way forward to introduce students to research early.

    Ladda ner fulltext (pdf)
    fulltext
  • 20.
    Forsberg, Håkan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Schwierz, Andreas
    Technische Hochschule Ingolstadt, Germany.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Assurance Strategy for New Computing Platforms in Safety-Critical Avionics2019Ingår i: Aerospace Technology Congress 2019 FT2019, Stockholm, Sweden, 2019, s. 137-144Konferensbidrag (Refereegranskat)
    Abstract [en]

    An assurance strategy for new computing platforms in safety-critical avionics has to be flexible and take into account different types of commercial-of-the-shelf (COTS) hardware technologies. Completely new COTS technologies are already being introduced and successfully used in other domains. Good examples are heterogeneous platforms, hardware-based machine learning and approximate computing. Current avionics certification guidance material cannot cope with next generation of devices. We suggest using the generic assurance approach of the Overarching Properties (OPs) together with assurance cases to argument that COTS assurance objectives are met and to achieve the flexibility required for future computing platforms. We introduce a novel assurance cased-based OP approach in [1] and refine the work into a framework in [2]. Within this framework we are able to integrate COTS technology specific assurance objectives using a five-step process. In this paper, we show through some representative examples of emerging computing platforms that our strategy is a way forward for new platforms in safety-critical avionics.

  • 21.
    Forsberg, Kristina
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. Saab AB, Sweden.
    Mårbring Isaksson, Eva
    Saab AB, Sweden.
    Gallina, Barbara
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Penna, Achille
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Elaboration of Safety Requirements2013Ingår i: AIAA/IEEE Digital Avionics Systems Conference - Proceedings2013, 2013, s. 7C21-7C29Konferensbidrag (Refereegranskat)
    Abstract [en]

    According to the aircraft standard ARP4754A, requirements should be carefully traced and validated. A systematic methodology for safety requirements elaboration (refinement/decomposition as well as allocation management) is lacking. To overcome this lack, an ARP-aligned and DOORS implementable approach called RAP (Requirements Allocation Process) is proposed. RAP offers a textual as well as graphical means for managing safety requirements. Besides supporting requirements decomposition and allocation, RAP also supports design decisions. The usefulness of RAP is illustrated by an example, applying the approach to a High Lift System.

  • 22.
    Fotouhi, Hossein
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Causevic, Adnan
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Björkman, Mats
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Communication and Security in Health Monitoring Systems - A Review2016Ingår i: Proceedings - International Computer Software and Applications Conference, 2016, s. 545-554Konferensbidrag (Refereegranskat)
    Abstract [en]

    The fast development of sensing devices and radios enables more powerful and flexible remote health monitoring systems. Considering the future vision of the Internet of Things (IoT), many requirements and challenges rise to the design and implementation of such systems. Bridging the gap between sensor nodes on the human body and the Internet becomes a challenging task in terms of reliable communications. Additionally, the systems will not only have to provide functionality, but also be highly secure. In this paper, we provide a survey on existing communication protocols and security issues related to pervasive health monitoring, describing their limitations, challenges, and possible solutions. We propose a generic protocol stack design as a first step toward handling interoperability in heterogeneous low-power wireless body area networks.

  • 23.
    Gallina, Barbara
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Gallucci, Antonio
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Nyberg, Mattias
    Scania, Sweden.
    VROOM & cC: a Method to Build Safety Cases for ISO 26262-compliant Product Lines2013Ingår i: Proceedings of SASSUR@SAFECOMP. 2013, 2013Konferensbidrag (Refereegranskat)
  • 24.
    Gallina, Barbara
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    THRUST: A method for speeding up the creation of process-related deliverables2014Konferensbidrag (Refereegranskat)
    Abstract [en]

    Certification of safety-critical avionics systems is an expensive and time-consuming activity due to the necessity of providing numerous deliverables. Some of these deliverables are process-related. To reduce time and cost related to the provision of process-related deliverables, in this paper, we propose to combine three approaches: the safety-oriented process line engineering approach, the process-based argumentation line approach, and the model driven certification-oriented approach. More specifically, we focus on safety-related processes for the development of avionics systems and we define how these three approaches are combined and which techniques, tools and guidelines should be used to implement the resulting approach, called THRUST. Advantages and disadvantages of possible existing techniques and tools are discussed and proposals as well as conceptual solutions for new techniques are sketched. Based on the sketched conceptual solutions, we then apply THRUST to speed up the creation of process-related deliverables in compliance with DO-178B/C.

  • 25.
    Gallina, Barbara
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Pitchai, K. R.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    S-TunExSPEM: Towards an extension of SPEM 2.0 to model and exchange tunable safety-oriented processes2014Ingår i: Software Engineering Research, Management and Applications, Springer, 2014, s. 215-230Kapitel i bok, del av antologi (Refereegranskat)
    Abstract [en]

    Prescriptive process-based safety standards (e.g. EN 50128, DO-178B, etc.) incorporate best practices to be adopted to develop safety-critical systems or software. In some domains, compliance with the standards is required to get the certificate from the certification authorities. Thus, a well-defined interpretation of the processes to be adopted is essential for certification purposes. Currently, no satisfying means allows process engineers and safety managers to model and exchange safety-oriented processes. To overcome this limitation, this paper proposes S-TunExSPEM, an extension of Software & Systems Process Engineering Meta-Model 2.0 (SPEM 2.0) to allow users to specify safety-oriented processes for the development of safety-critical systems in the context of safety standards according to the required safety level. Moreover, to enable exchange for simulation, monitoring, execution purposes, S-TunExSPEM concepts are mapped onto XML Process Definition Language 2.2 (XPDL 2.2) concepts. Finally, a case-study from the avionics domain illustrates the usage and effectiveness of the proposed extension.

  • 26.
    Gu, Rong
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Marinescu, Raluca
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Seceleanu, Cristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Formal verification of an Autonomous Wheel Loader by model checking2018Ingår i: Proceedings - International Conference on Software Engineering, IEEE Computer Society , 2018, s. 74-83Konferensbidrag (Refereegranskat)
    Abstract [en]

    In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks autonomously, the machines are equipped with different features, such as position localization, human and obstacle detection, collision avoidance, etc. Such systems are safety critical, and should operate autonomously with very high dependability (e.g., by meeting task deadlines, avoiding (fatal) accidents at all costs, etc.). An Autonomous Wheel Loader is a machine that transports materials within the construction site without a human in the cab. To check the dependability of the loader, in this paper we provide a timed automata description of the vehicle's control system, including the abstracted path planning and collision avoidance algorithms used to navigate the loader, and we model check the encoding in UPPAAL, against various functional, timing and safety requirements. The complex nature of the navigation algorithms makes the loader's abstract modeling and the verification very challenging. Our work shows that exhaustive verification techniques can be applied early in the development of autonomous systems, to enable finding potential design errors that would incur increased costs if discovered later.

  • 27.
    Gu, Rong
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Marinescu, Raluca
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Seceleanu, Cristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Towards a Two-layer Framework for Verifying Autonomous Vehicles2019Ingår i: NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science, vol 11460, 2019Konferensbidrag (Refereegranskat)
    Abstract [en]

    Autonomous vehicles rely heavily on intelligent algorithms for path planning and collision avoidance, and their functionality and dependability could be ensured through formal verification. To facilitate the verification, it is beneficial to decouple the static high-level planning from the dynamic functions like collision avoidance. In this paper, we propose a conceptual two-layer framework for verifying autonomous vehicles, which consists of a static layer and a dynamic layer. We focus concretely on modeling and verifying the dynamic layer using hybrid automata and UPPAAL SMC, where a continuous movement of the vehicle as well as collision avoidance via a dipole flow field algorithm are considered. This framework achieves decoupling by separating the verification of the vehicle's autonomous path planning from that of the vehicle autonomous operation in a continuous dynamic environment. To simplify the modeling process, we propose a pattern-based design method, where patterns are expressed as hybrid automata. We demonstrate the applicability of the dynamic layer of our framework on an industrial prototype of an autonomous wheel loader.

  • 28.
    Hansson, Hans
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Carlson, Jan
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Isovic, Damir
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Nolte, Thomas
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Ouimet, Martin
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Punnekkat, Sasikumar
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Seceleanu, Cristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Real-Time Systems2010Bok (Övrigt vetenskapligt)
    Abstract [en]

    This is a textbook developed for use in the Master Programme Module E-M.6 "Real-Time Systems" as part of the Postgraduate Distance studies organized by Fraunhofer IESE and the Distance and International Studies Center at the Technical University of Kaiserslauten, Germany.

  • 29.
    Hansson, Hans
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Nolte, Thomas
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Axelsson, Jakob
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Björkman, Mats
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Carlson, Jan
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Crnkovic, Ivica
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lisper, Björn
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Norström, Christer
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Punnekkat, Sasikumar
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Sjödin, Mikael
    Mälardalens högskola, Akademin för innovation, design och teknik.
    The PROGRESS Centre for Predictable Embedded Software Systems - Half-time report (edited version)2010Rapport (Övrigt vetenskapligt)
    Abstract [en]

    Presentation of the achievements and activities within the PROGRESS national strategic research centre 2006-2008

  • 30.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Dodig-Crnkovic, Gordana
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Hänninen, Kaj
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Risk-based decision-making fallacies: Why present functional safety standards are not enough2017Ingår i: Proceedings - 2017 IEEE International Conference on Software Architecture Workshops, ICSAW 2017: Side Track Proceedings, Institute of Electrical and Electronics Engineers Inc. , 2017, s. 153-160Konferensbidrag (Refereegranskat)
    Abstract [en]

    Functional safety of a system is the part of its overall safety that depends on the system operating correctly in response to its inputs. Safety is defined as the absence of unacceptable/unreasonable risk by functional safety standards, which enforce safety requirements in each phase of the development process of safety-critical software and hardware systems. Acceptability of risks is judged within a framework of analysis with contextual and cultural aspects by individuals who may introduce subjectivity and misconceptions in the assessment. While functional safety standards elaborate much on the avoidance of unreasonable risk in the development of safety-critical software and hardware systems, little is addressed on the issue of avoiding unreasonable judgments of risk. Through the studies of common fallacies in risk perception and ethics, we present a moral-psychological analysis of functional safety standards and propose plausible improvements of the involved risk-related decision making processes, with a focus on the notion of an acceptable residual risk. As a functional safety reference model, we use the functional safety standard ISO 26262, which addresses potential hazards caused by malfunctions of software and hardware systems within road vehicles and defines safety measures that are required to achieve an acceptable level of safety. The analysis points out the critical importance of a robust safety culture with developed countermeasures to the common fallacies in risk perception, which are not addressed by contemporary functional safety standards. We argue that functional safety standards should be complemented with the analysis of potential hazards caused by fallacies in risk perception, their countermeasures, and the requirement that residual risks must be explicated, motivated, and accompanied by a plan for their continuous reduction. This approach becomes especially important in contemporary developed autonomous vehicles with increasing computational control by increasingly intelligent software applications.

  • 31.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik. Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Kristina, Lundqvist
    Mälardalens högskola, Akademin för innovation, design och teknik. Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik. Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Hänninen, Kaj
    Mälardalens högskola, Akademin för innovation, design och teknik. Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Regression verification of AADL models through slicing of system dependence graphs2014Ingår i: QoSA 2014 - Proceedings of the 10th International ACM SIGSOFT Conference on Quality of Software Architectures (Part of CompArch 2014), 2014, s. 103-112Konferensbidrag (Refereegranskat)
    Abstract [en]

    Design artifacts of embedded systems are subjected to a number of modifications during the development process. Verified artifacts that subsequently are modified must nec- essarily be re-Verified to ensure that no faults have been introduced in response to the modification. We collectively call this type of verification as regression verification. In this paper, we contribute with a technique for selective regression verification of embedded systems modeled in the Architec- ture Analysis and Design Language (AADL). The technique can be used with any AADL-based verification technique to eficiently perform regression verification by only selecting verification sequences that cover parts that are afiected by the modification for re-execution. This allows for the avoid- ance of unnecessary re-verification, and thereby unnecessary costs. The selection is based on the concept of specification slicing through system dependence graphs (SDGs) such that the efiect of a modification can be identified.

  • 32.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Developing dependable software-intensive systems: AADL vs. EAST-ADL2011Ingår i: Lecture Notes in Computer Science, vol. 6652, Springer, 2011, s. 103-117Kapitel i bok, del av antologi (Refereegranskat)
    Abstract [en]

    Dependable software-intensive systems, such as embedded systems for avionics and vehicles are often developed under severe quality, schedule and budget constraints. As the size and complexity of these systems dramatically increases, the architecture design phase becomes more and more significant in order to meet these constraints. The use of Architecture Description Languages (ADLs) provides an important basis for mutual communication, analysis and evaluation activities. Hence, selecting an ADL suitable for such activities is of great importance. In this paper we compare and investigate the two ADLs - AADL and EAST-ADL. The level of support provided to developers of dependable software-intensive systems is compared, and several critical areas of the ADLs are highlighted. Results of using an extended comparison framework showed many similarities, but also one clear distinction between the languages regarding the perspectives and the levels of abstraction in which systems are modeled. © 2011 Springer-Verlag.

  • 33.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Hänninen, Kaj
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    AQAT: The Architecture Quality Assurance Tool for Critical Embedded Systems2017Ingår i: Proceedings - International Symposium on Software Reliability Engineering, ISSRE, Volume 2017, 2017, s. 260-270, artikel-id 8109092Konferensbidrag (Refereegranskat)
    Abstract [en]

    Architectural engineering of embedded systems comprehensively affects both the development processes and the abilities of the systems. Verification of architectural engineering is consequently essential in the development of safety- and mission-critical embedded system to avoid costly and hazardous faults. In this paper, we present the Architecture Quality Assurance Tool (AQAT), an application program developed to provide a holistic, formal, and automatic verification process for architectural engineering of critical embedded systems. AQAT includes architectural model checking, model-based testing, and selective regression verification features to effectively and efficiently detect design faults, implementation faults, and faults created by maintenance modifications. Furthermore, the tool includes a feature that analyzes architectural dependencies, which in addition to providing essential information for impact analyzes of architectural design changes may be used for hazard analysis, such as the identification of potential error propagations, common cause failures, and single point failures. Overviews of both the graphical user interface and the back-end processes of AQAT are presented with a sensor-to-actuator system example.

  • 34.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Hänninen, Kaj
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Torelm, M.
    Bombardier Transportation Sweden AB, Västerås, Sweden.
    AQAF: An architecture quality assurance framework for systems modeled in AADL2016Ingår i: Proceedings - 2016 12th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2016, 2016, s. 31-40Konferensbidrag (Refereegranskat)
    Abstract [en]

    Architecture engineering is essential to achieve dependability of critical embedded systems and affects large parts of the system life cycle. There is consequently little room for faults, which may cause substantial costs and devastating harm. Verification in architecture engineering should therefore be holistically and systematically managed in the development of critical embedded systems, from requirements analysis and design to implementation and maintenance. In this paper, we address this problem by presenting AQAF: an Architecture Quality Assurance Framework for critical embedded systems modeled in the Architecture Analysis and Design Language (AADL). The framework provides a holistic set of verification techniques with a common formalism and semantic domain, architecture flow graphs and timed automata, enabling completely formal and automated verification processes covering virtually the entire life cycle. The effectiveness and efficiency of the framework are validated in a case study comprising a safety-critical train control system. 

  • 35.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Architecture-Based Regression Verification of AADL SpecificationsManuskript (preprint) (Övrigt vetenskapligt)
    Abstract [en]

    Design artifacts of dependable embedded systems, and the systems themselves, are subjected to a number of modifications during the development process. Verified artifacts that subsequently are modified must necessarily be re-verified to ensure that no faults have been introduced in response to the modification. We collectively call this type of verification as regression verification. Studies show that regression testing alone consumes a vast amount of the total development cost. This is likely a result of unnecessary verification of parts that are not affected by the modification. In this paper, we propose an architecture-based selective regression verification technique for the development process of dependable embedded systems specified in the Architecture Analysis and Design Language (AADL). The selection of necessary regression verification sequences is based on the concept of specification slicing through System Dependence Graphs (SDGs). This allows for the avoidance of unnecessary re-verification, and thereby unnecessary costs.

  • 36.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Hänninen, Kaj
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Torelm, Martin
    Bombardier Transp., Sweden .
    Experience Report: Evaluating Fault Detection Effectiveness and Resource Efficiency of the Architecture Quality Assurance Framework and Tool2017Ingår i: Proceedings - International Symposium on Software Reliability Engineering, ISSRE. Volume 2017, 2017, s. 271-281, artikel-id 8109093Konferensbidrag (Refereegranskat)
    Abstract [en]

    The Architecture Quality Assurance Framework (AQAF) is a theory developed to provide a holistic and formal verification process for architectural engineering of critical embedded systems. AQAF encompasses integrated architectural model checking, model-based testing, and selective regression verification techniques to achieve this goal. The Architecture Quality Assurance Tool (AQAT) implements the theory of AQAF and enables automated application of the framework. In this paper, we present an evaluation of AQAT and the underlying AQAF theory by means of an industrial case study, where resource efficiency and fault detection effectiveness are the targeted properties of evaluation. The method of fault injection is utilized to guarantee coverage of fault types and to generate a data sample size adequate for statistical analysis. We discovered important areas of improvement in this study, which required further development of the framework before satisfactory results could be achieved. The final results present a 100% fault detection rate at the design level, a 98.5% fault detection rate at the implementation level, and an average increased efficiency of 6.4% with the aid of the selective regression verification technique.

  • 37.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Jaradat, Omar
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Automated Verification of AADL-Specifications Using UPPAAL2012Ingår i: Proceedings of the 14th IEEE International Symposium on High Assurance Systems Engineering (HASE), 2012, s. 130-138Konferensbidrag (Refereegranskat)
    Abstract [en]

    The Architecture Analysis and Design Language (AADL) is used to represent architecture design decisions of safety-critical and real-time embedded systems. Due to the far-reaching effects these decisions have on the development process, an architecture design fault is likely to have a significant deteriorating impact through the complete process. Automated fault avoidance of architecture design decisions therefore has the potential to significantly reduce the cost of the development while increasing the dependability of the end product. To provide means for automated fault avoidance when developing systems specified in AADL, a formal verification technique has been developed to ensure completeness and consistency of an AADL specification as well as its conformity with the end product. The approach requires the semantics of AADL to be formalized and implemented. We use the methodology of semantic anchoring to contribute with a formal and implemented semantics of a subset of AADL through a set of transformation rules to timed automata constructs. In addition, the verification technique, including the transformation rules, is validated using a case study of a safety-critical fuel-level system developed by a major vehicle manufacturer.

  • 38.
    Johnsen, Andreas
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    An Architecture-Based Verification Technique for AADL Specifications2011Konferensbidrag (Refereegranskat)
    Abstract [en]

    Quality assurance processes of software-intensive systems are an increasing challenge as the complexity of these systems dramatically increases. The use of Architecture Description Languages (ADLs) provide an important basis for evaluation. The Architecture Analysis and Design Language (AADL) is an ADL developed for designing software intensive systems. In this paper, we propose an architecture-based verification technique covering the entire development process by adapting a combination of model-checking and model-based testing approaches to AADL specifications. The technique reveals inconsistencies of early design decisions and ensures a system's conformity with its AADL specification. The objective and criteria (test-selection) of the verification technique is derived from traditional integration testing.

  • 39.
    Kienle, Holger
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Sundmark, Daniel
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Johnsen, Andreas
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Liability for Software in Safety-Critical Mechatronic Systems: An Industrial Questionnaire2012Ingår i: 2012 2nd International Workshop on Software Engineering for Embedded Systems, SEES 2012 - Proceedings, 2012, s. 44-50Konferensbidrag (Refereegranskat)
    Abstract [en]

    There is very little research on how industry is dealing with the risk of legal liability when constructing safety- critical mechatronic systems that are also software intensive. In this paper we propose a case study approach with the goal to understand how liability concerns in this setting impact software development in industry. The approach takes into account that software development is embedded into a complex socio-technical context involving stakeholders from technical, managerial and legal backgrounds. We present first results of our case study from a questionnaire involving six companies that develop software- intensive, safety-critical systems in the vehicular and avionics domains. The results of the questionnaire shed light on current industrial practices and concerns. The results indicate that liability seems indeed a concern and that a more in-depth analysis of this topic would be desirable to better understand the strategies that are used by industry to address liability risks.

  • 40.
    Lundqvist, Kristina
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Towards System-level Fault-tolerance Using Formal Methods And Soc Methodologies2007Ingår i: Unique Chips and Systems, CRC Press, 2007, s. 299-324Kapitel i bok, del av antologi (Övrigt vetenskapligt)
  • 41.
    Lundqvist, Kristina
    et al.
    Uppsala Univ., Sweden.
    Asplund, Lars
    Uppsala Univ., Sweden.
    A Formal Model of a Run-Time Kernel for Ravenscar1999Ingår i: Proc. 6th International Conference on Real-Time Computing Systems and Applications - RTCSA'99, Hong-Kong, 1999, s. 504-507Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    The Ravenscar tasking profile for Ada 95 has been designed to allow implementation of highly safety critical systems in Ada. Ravenscar defines a tasking run-time system with deterministic behaviour and low complexity. We provide a formal model of the primitives provided by Ravenscar including exceptions. This formal model can be used to verify safety properties of applications targeting a Ravenscar-compliant run-time system. As an illustration of this, we model a sample application using all features of Ravenscar and formally verify its correctness using the real-time model checker UPPAAL

  • 42.
    Lundqvist, Kristina
    et al.
    Uppsala University, Sweden.
    Asplund, Lars
    Uppsala University, Sweden.
    A Formal Model of the Ada Ravenscar Tasking Profile; Delay Until1999Ingår i: Proc. ACM SIGAda Annual International Conference'99, 1999, s. 15-21Konferensbidrag (Övrigt vetenskapligt)
    Abstract [en]

    The definition of the Ravenscar Tasking Profile for Ada 95 provides a definition of a tasking runtime system with deterministic behaviour and low enough complexity to permit a formal description and verification of the model. A complete run-time system is being modeled using the real-time model checker UPPAAL, and this work describes the handling of delay until. Since scheduling is not yet modelled a simple non-preemptive scheduler has been used when verifying the delay queue.

  • 43.
    Lundqvist, Kristina
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Asplund, Lars
    Mälardalens högskola, Akademin för innovation, design och teknik.
    A Ravenscar-Compliant Run-Time Kernel for Safety-Critical Systems2003Ingår i: The International Journal of Time-Critical Comuting, Vol. 24, nr 1, s. 29-54Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The Ravenscar tasking profile for Ada 95 has been designed to allow implementation of highly safety critical systems. Ravenscar defines a tasking system with deterministic behavior and low complexity. We provide a formal model using UPPAAL of the primitives provided by Ravenscar including exceptions. This formal model is used to verify the correctness of the Ravenscar model and can be used to verify safety properties of applications using the Ravenscar profile. As an illustration of this, we model a sample application using all features of Ravenscar and formally verify its correctness. Furthermore, an introduction to the Ravenscar model is given.

  • 44.
    Lundqvist, Kristina
    et al.
    Uppsala University, Uppsala, Sweden.
    Asplund, Lars
    Uppsala University, Uppsala, Sweden.
    Michell, Stephen
    Maurya Software, Ontario, Canada.
    A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects1999Ingår i: Proc. Reliable Software Technologies, Ada-Europe'99, LNCS 1622, 1999, s. 12-25Konferensbidrag (Övrigt vetenskapligt)
  • 45.
    Lundqvist, Kristina
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Srinivasan, J.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Why is Aerospace Software Development and Sustainment Hard?2005Övrigt (Övrigt vetenskapligt)
  • 46.
    Lundqvist, Kristina
    et al.
    Massachusetts Institute of Technology, United States.
    Srinivasan, Jayakanth
    Massachusetts Institute of Technology, United States.
    A First Course in Software Engineering for Aerospace Engineers2006Ingår i: Software Engineering Education Conference, Proceedings, Volume 2006, 2006, s. 77-84Konferensbidrag (Övrigt vetenskapligt)
  • 47.
    Lundqvist, Kristina
    et al.
    Massachusetts Institute of Technology, USA.
    Srinivasan, Jayakanth
    Massachusetts Institute of Technology, USA.
    Gorelov, Sebastien
    Massachusetts Institute of Technology, USA.
    Non-Intrusive System-Level Fault Tolerance2005Ingår i: Lecture Notes in Computer Science, Volume 3555, 2005, s. 156-166Konferensbidrag (Övrigt vetenskapligt)
  • 48.
    Lundqvist, Kristina
    et al.
    Uppsala universitet.
    Wall, Göran
    Uppsala universitet.
    A Rendezvous with Linda1997Ingår i: ACM SIGAda Letters, ISSN 1094-3641, Vol. XVII, nr 3, s. 87-96Artikel i tidskrift (Refereegranskat)
  • 49. Lundqvist, Kristina
    et al.
    Wall, Göran
    A Rendezvous with Linda1996Ingår i: Proc. Washington Ada Symposium'96, 1996Konferensbidrag (Övrigt vetenskapligt)
  • 50.
    Lundqvist, Kristina
    et al.
    Uppsala University, Sweden.
    Wall, Göran
    Uppsala University, Sweden.
    Using Object Oriented Methods in Ada 95 to implement Linda1996Ingår i: Lecture Notes in Computer Science, Volume 1088, 1996, s. 211-222Konferensbidrag (Övrigt vetenskapligt)
123 1 - 50 av 112
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf