| 1. |
- Gurov, Dilian, 1964-, et al.
(författare)
-
A Hoare Logic Contract Theory : An Exercise in Denotational Semantics
- 2018
-
Ingår i: Principled Software Development. - Cham : Springer Nature. ; , s. 119-127
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- We sketch a simple theory of Hoare logic contracts for programs with procedures, presented in denotational semantics. In particular, we give a simple semantic justification of the usual procedure-modular treatment of such programs. The justification is given by means of a proof of soundness of a contract-relative denotational semantics against the standard denotational semantics of procedures in the context of procedure declarations. The suggested formal development can be used as an inspiration for more ambitious contract theories.
|
|
| 2. |
- Gurov, Dilian, et al.
(författare)
-
Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report
- 2017
-
Ingår i: Critical Systems: Formal Methods and Automated Verification. - Cham : Springer. - 9783319671130 - 9783319671123 ; , s. 3-18
-
Konferensbidrag (refereegranskat)abstract
- This paper summarizes our experiences from an exercise in deductive verification of functional properties of automotive embedded Ccode in an industrial setting. We propose a formal requirements model that supports the way C-code requirements are currently written at Scania. We describe our work, for a safety-critical module of an embedded system, on formalizing its functional requirements and verifying its C-code implementation by means of VCC, an established tool for deductive verification. We describe the obstacles we encountered, and discuss the automation of the specification and annotation effort as a prerequisite for integrating this technology into the embedded software design process.
|
|
| 3. |
- Nord, Tora, 1976-, et al.
(författare)
-
Vad är en arbetsmarknad?
- 2020. - 1
-
Ingår i: Vad är arbetsvetenskap?. - Lund : Studentlitteratur AB. - 9789144122489 ; , s. 91-108
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)
|
|
| 4. |
- Nyberg, Mattias, et al.
(författare)
-
Formal verification in automotive industry : Enablers and obstacles
- 2018
-
Ingår i: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018. - Cham : Springer. - 9783030034269 ; , s. 139-158
-
Konferensbidrag (refereegranskat)abstract
- We describe and summarize our experiences from six industrial case studies in applying formal verification techniques to embedded, safety-critical code. The studies were conducted at Scania over the period of eight years. Despite certain successes, we have so far failed to introduce formal techniques on a larger scale. Based on our experiences, we identify and discuss some key obstacles to, and enabling factors for the successful incorporation of formal verification techniques into the software development and quality assurance process.
|
|
| 5. |
- Nyberg, Mattias, et al.
(författare)
-
Formally Proving Compositionality in Industrial Systems with Informal Specifications
- 2020
-
Ingår i: ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Applications. - Cham : Springer Science and Business Media Deutschland GmbH. ; , s. 348-365
-
Konferensbidrag (refereegranskat)abstract
- Based upon first-order logic, the paper presents a methodology and a deductive system for proving compositionality. Typical specifications found in industry are not expressed in any formal notation; rather most often in natural language. Therefore, the methodology does not assume specifications to be formal logical sentences. Instead, the methodology takes as input, properties of specifications and in particular, refinement relations. To cover general industrial heterogeneous systems, the semantics chosen is behavior based, originating in previous work on contract-based design for cyber-physical systems. In contrast to the previous work, implementation of specifications is non-monotonic with respect to composition. That is, even though a specification is implemented by one component, a composition with a second component may not implement the same specification. This kind of non-monotonicity is fundamentally important to support architectural specifications and so-called freedom-of-interference used in design of safety critical systems.
|
|
| 6. |
- Törngren, Martin, 1963-, et al.
(författare)
-
Architecting Safety Supervisors for High Levels of Automated Driving
- 2018
-
Ingår i: Proceeding of the 21st IEEE Int. Conf. on Intelligent Transportation Systems. - : IEEE.
-
Konferensbidrag (refereegranskat)abstract
- The complexity of automated driving poses challenges for providing safety assurance. Focusing on the architecting of an Autonomous Driving Intelligence (ADI), i.e. the computational intelligence, sensors and communication needed for high levels of automated driving, we investigate so called safety supervisors that complement the nominal functionality. We present a problem formulation and a functional architecture of a fault-tolerant ADI that encompasses a nominal and a safety supervisor channel. We then discuss the sources of hazardous events, the division of responsibilities among the channels, and when the supervisor should take over. We conclude with identified directions for further work.
|
|
| 7. |
- Westman, Jonas, 1986-, et al.
(författare)
-
Conditions of Contracts for Separating Responsibilities in Heterogeneous Systems
- 2018
-
Ingår i: Formal methods in system design. - : Springer Nature. - 0925-9856 .- 1572-8102. ; 52:2, s. 147-192
-
Tidskriftsartikel (refereegranskat)abstract
- A general, compositional, and component-based contract theory is proposed for modeling and specifying heterogeneous systems, characterized by consisting of parts from different domains, e.g. software, electrical and mechanical. Given a contract consisting of assumptions and a guarantee, clearly separated conditions on a component and its environment are presented where the conditions ensure that the guarantee is fulfilled - a responsibility assigned to the component, given that the environment fulfills the assumptions. The conditions are applicable whenever it cannot be ensured that the sets of ports of components are partitioned into inputs and outputs, and hence fully support scenarios where components, characterized by both causal and acausal models, are to be integrated by solely relying on the information of a contract. An example of such a scenario of industrial relevance is explicitly considered, namely a scenario in a supply chain where the development of a component is outsourced. To facilitate the application of the theory in practice, necessary properties of contracts are also derived to serve as sanity checks of the conditions. Furthermore, based on a graph that represents a structuring of a hierarchy of contracts, sufficient conditions to achieve compositionality are presented.
|
|
| 8. |
- Westman, Jonas, 1986-, et al.
(författare)
-
Contracts for Specifying and Structuring Requirements on Cyber-Physical Systems
- 2015
-
Ingår i: Cyber-Physical Systems. - : CRC Press. ; , s. 307-342
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- The notion of contracts was first introduced in Meyer [67] as a pair of pre-and postconditions [36, 45, 57] to be used in formal specification of software (SW) interfaces. In recent work [12,14], developed within the European research project SPEEDS [85], the use of contracts is extended from formal specification of software to serving as a central design philosophy in systems engineering to support the design of cyber-physical systems (CPS) [60,81]. One of the key challenges that triggered the extension of contracts is the increasingly complex development environment of cyberphysical systems, characterized by distributed original equipment manufacturer (OEM)/supplier chains [12, 14].
|
|
| 9. |
- Westman, Jonas, 1986-, et al.
(författare)
-
Contracts for Structuring and Specifying Requirements on Cyber-Physical Systems
- 2015
-
Ingår i: Cyber-Physical Systems<em><em></em></em>. - : CRC Press. - 9781482263329
-
Bokkapitel (refereegranskat)abstract
- A contract splits the responsibilities between a component and its environment into a guarantee that expresses an intended property under the responsibility of the component, given that the environment fulfills the assumptions. Building on recent works where contracts are proposed as a means to meet the challenges in the design of Cyber-Physical Systems (CPSs), a general contract framework is presented that supports the modelling of both individual components and architectures of CPS - at all levels of design, as well as the structuring and specification of requirements on the components using contracts. To facilitate the specification of requirements, constraints that restrict the portsover which a contract is expressed are introduced to serve as sanity checks that the component and the environment meet their respective responsibilities. Furthermore, a new graph, called a \emph{contract structure} is introduced to support the structuring and tracing of requirements on a CPS using contracts. As a proof-of-concept, the framework is used to specify and structure safety requirements on an industrial system, as proposed by ISO 26262.
|
|
| 10. |
- Westman, Jonas, 1986-, et al.
(författare)
-
CPS Specifier - A Specification Tool for Safety-Critical Cyber-Physical Systems
- 2016
-
Konferensbidrag (refereegranskat)abstract
- CPS Specifier is a specification tool for Cyber-Physical Systems. Founded on established theory and realized using general design and integration technologies and principles, e.g. Linked Data, CPS Specifier provides guidance-and feedback-driven support when authoring structured specifications in general, and for specifying and structuring requirements, in particular. The provided support is crucial in order to comply with functional safety standards such as IEC 61508 and ISO 26262 that require particularly stringent requirements engineering.
|
|
