| 1. |
- Calinescu, Radu, et al.
(author)
-
Synthesis and Verification of Self-aware Computing Systems
- 2017
-
In: Self-aware Computing Systems. - Cham : Springer. - 9783319474724 ; , s. 337-373
-
Book chapter (other academic/artistic)abstract
- Self-aware computing systems are envisaged to exploit the knowledge of their own software architecture, hardware infrastructure and environment in order to follow high-level goals through proactively adapting as their environment evolves. This chapter describes two classes of key enabling techniques for self-adaptive systems: automated synthesis and formal verification. The ability to dynamically synthesize component connectors and compositions underpins the proactive adaptation of the architecture of self-aware systems. Deciding when adaptation is needed and selecting valid new architectures or parameters for self-aware systems often requires formal verification. We present the state of the art in the use of the two techniques for the development of self-aware computing systems and summarize the main research challenges associated with their adoption in practice.
|
|
| 2. |
|
|
| 3. |
- Chen, Taolue, et al.
(author)
-
A Compositional Specification Theory for Component Behaviours
- 2012
-
In: Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783642288685 ; , s. 148-168
-
Conference paper (peer-reviewed)abstract
- We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks.
|
|
| 4. |
|
|
| 5. |
- Chilton, Chris, et al.
(author)
-
An algebraic theory of interface automata
- 2014
-
In: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 549, s. 146-174
-
Journal article (peer-reviewed)abstract
- We formulate a compositional specification theory for interface automata, where a component model specifies the allowed sequences of input and output interactions with the environment. A trace-based linear-time refinement is provided, which is the weakest preorder preserving substitutivity of components, and is weaker than the classical alternating simulation defined on interface automata. Since our refinement allows a component to be refined by refusing to produce any output, we also define a refinement relation that guarantees safety and progress. The theory includes the operations of parallel composition to support the structural composition of components, logical conjunction and disjunction for independent development, hiding to support abstraction of interfaces, and quotient for incremental synthesis of components. Our component formulation highlights the algebraic properties of the specification theory for both refinement preorders, and is shown to be fully abstract with respect to observation of communication mismatches. Examples of independent and incremental component development are provided.
|
|
| 6. |
- Chilton, Chris, et al.
(author)
-
Assume-Guarantee Reasoning for Safe Component Behaviours
- 2012
-
In: Proc. FACS: Formal Aspects of Component Software, 9th Int. Symp.. - Springer : Springer Berlin Heidelberg. ; , s. 92-109, s. 92-109
-
Conference paper (peer-reviewed)abstract
- We formulate a sound and complete assume-guarantee framework for reasoning compositionally about safety properties of component behaviours. The specification of a component, which constrains the temporal ordering of input and output interactions with the environment, is expressed in terms of two prefix-closed sets of traces: an assumption and guarantee. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated by considering a simple printing example.
|
|
| 7. |
- Chilton, Chris, et al.
(author)
-
Compositional assume–guarantee reasoning for input/output component theories
- 2014
-
In: Science of Computer Programming. - : Elsevier BV. - 0167-6423 .- 1872-7964. ; 91, s. 115-137
-
Journal article (peer-reviewed)abstract
- We formulate a sound and complete assume-guarantee framework for reasoning compositionally about components modelled as a variant of interface automata. The specification of a component, which expresses both safety and progress properties of input and output interactions with the environment, is characterised by finite traces. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction and disjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated through a link layer protocol case study.
|
|
| 8. |
|
|
| 9. |
- Sejersen, Thomas, et al.
(author)
-
Healthcare resource utilisation and direct medical cost for individuals with 5q spinal muscular atrophy in Sweden
- 2024
-
In: EUROPEAN JOURNAL OF HEALTH ECONOMICS. - 1618-7598 .- 1618-7601.
-
Journal article (peer-reviewed)abstract
- Background Spinal muscular atrophy (SMA) is a rare, progressive, neuromuscular disorder. Recent advances in treatment require an updated assessment of burden to inform reimbursement decisions.Objectives To quantify healthcare resource utilisation (HCRU) and cost of care for patients with SMA.Methods Cohort study of patients with SMA identified in the Swedish National Patient Registry (2007-2018), matched to a reference cohort grouped into four SMA types (1, 2, 3, unspecified adult onset [UAO]). HCRU included inpatient admissions, outpatient visits, procedures, and dispensed medications. Direct medical costs were estimated by multiplying HCRU by respective unit costs. Average annual HCRU and medical costs were modelled for SMA versus reference cohorts to estimate differences attributable to the disease (i.e., average treatment effect estimand). The trajectory of direct costs over time were assessed using synthetic cohorts.Results We identified 290 SMA patients. Annualised HCRU was higher in SMA patients compared with reference cohorts. Highest risk ratios were observed for inpatient overnight stays for type 1 (risk ratio [RR]: 29.2; 95% confidence interval [CI]: 16.0, 53.5) and type 2 (RR: 23.3; 95% CI: 16.4,33.1). Mean annual direct medical costs per patient for each year since first diagnosis were greatest for type 1 (euro114,185 and SMA-attributable: euro113,380), type 2 (euro61,876 and SMA-attributable: euro61,237), type 3 (euro45,518 and SMA-attributable: euro44,556), and UAO (euro4046 and SMA-attributable: euro2098). Costs were greatest in the 2-3 years after the first diagnosis for all types.Discussion and conclusion The economic burden attributable to SMA is significant. Further research is needed to understand the burden in other European countries and the impact of new treatments.
|
|
| 10. |
- Senn, Pascal, et al.
(author)
-
NANOCI-Nanotechnology Based Cochlear Implant With Gapless Interface to Auditory Neurons
- 2017
-
In: Otology and Neurotology. - 1531-7129 .- 1537-4505. ; 38:8, s. E224-E231
-
Journal article (peer-reviewed)abstract
- Cochlear implants (CI) restore functional hearing in the majority of deaf patients. Despite the tremendous success of these devices, some limitations remain. The bottleneck for optimal electrical stimulation with CI is caused by the anatomical gap between the electrode array and the auditory neurons in the inner ear. As a consequence, current devices are limited through 1) low frequency resolution, hence suboptimal sound quality and 2), large stimulation currents, hence high energy consumption (responsible for significant battery costs and for impeding the development of fully implantable systems). A recently completed, multinational and interdisciplinary project called NANOCI aimed at overcoming current limitations by creating a gapless interface between auditory nerve fibers and the cochlear implant electrode array. This ambitious goal was achieved in vivo by neurotrophin-induced attraction of neurites through an intra-cochlear gel-nanomatrix onto a modified nanoCI electrode array located in the scala tympani of deafened guinea pigs. Functionally, the gapless interface led to lower stimulation thresholds and a larger dynamic range in vivo, and to reduced stimulation energy requirement (up to fivefold) in an in vitro model using auditory neurons cultured on multi-electrode arrays. In conclusion, the NANOCI project yielded proof of concept that a gapless interface between auditory neurons and cochlear implant electrode arrays is feasible. These findings may be of relevance for the development of future CI systems with better sound quality and performance and lower energy consumption. The present overview/review paper summarizes the NANOCI project history and highlights achievements of the individual work packages.
|
|
