Harald Ruess

We present a principled approach to engineering cyber–physical systems (CPS) based on a semantically coherent framework of models for specifying, abstracting, designing, refining, and implementing software-intensive CPS. This framework supports essential systems and software engineering principles, such as encapsulation, information hiding, modular composition, and traceability.

Seeking a significant shift in the traditional software development and verification paradigm.

We argue that relative importance and its equitable attribution in terms of Shapley-Owen effects is an appropriate one, and, if we accept a small number of reasonable imperatives for equitable attribution, the only way to measure fairness. On the other hand, the computation of Shapley-Owen effects can be very demanding. Our main technical result is a spectral decomposition of the Shapley-Owen effects, which decomposes the computation of these indices into a model-specific and a model-independent part. The model-independent part is precomputed once and for all, and the model-specific computation of Shapley-Owen effects is expressed analytically in terms of the coefficients of the model's \emph{polynomial chaos expansion} (PCE), which can now be reused to compute different Shapley-Owen effects. We also propose an algorithm for computing precise and sparse truncations of the PCE of the model and the spectral decomposition of the Shapley-Owen effects, together with upper bounds on the accumulated approximation errors. The approximations of both the PCE and the Shapley-Owen effects converge to their true values.

Our main result is a doubly exponential decision procedure for the first-order equality theory of streams with addition, convolution, and control-oriented stream operations. This stream logic is shown to be expressive for solving basic problems in stream calculus.

The main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is expressive for elementary problems of stream calculus.

Covariate shift may impact the operational safety performance of neural networks. A re-evaluation of the safety performance, however, requires collecting new operational data and creating corresponding ground truth labels, which often is not possible during operation. We are therefore proposing to reshape the initial test set, as used for the safety performance evaluation prior to deployment, based on an approximation of the operational data. This approximation is obtained by observing and learning the distribution of activation patterns of neurons in the network during operation. The reshaped test set reflects the distribution of neuron activation values as observed during operation, and may therefore be used for re-evaluating safety performance in the presence of covariate shift. First, we derive conservative bounds on the values of neurons by applying finite binning and static dataflow analysis. Second, we formulate a mixed integer linear programming (MILP) constraint for constructing the minimum set of data points to be removed in the test set, such that the difference between the discretized test and operational distributions is bounded. We discuss potential benefits and limitations of this constraint-based approach based on our initial experience with an implemented research prototype.

Cyberlogic is an enabling logical foundation for building and analyzing digital transactions that involve the exchange of digital forms of evidence. It is based on an extension of (first-order) intuitionistic predicate logic with an attestation and a knowledge modality. The key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are specified as distributed logic programs, and (3) verifiable evidence is collected by means of distributed proof search. Verifiable evidence, in particular, are constructed from extra-logical elements such as signed documents and cryptographic signatures. Despite this conceptual simplicity of Cyberlogic, central features of authorization policies including trust, delegation, and revocation of authority are definable. An expressive temporal-epistemic logic for specifying distributed authorization policies and protocols is therefore definable in Cyberlogic using a trusted time source. We describe the distributed execution of Cyberlogic programs based on the hereditary Harrop fragment in terms of distributed proof search, and we illustrate some fundamental issues in the distributed construction of certificates. The main principles of encoding and executing cryptographic protocols in Cyberlogic are demonstrated. Finally, a functional encryption scheme is proposed for checking certificates of evidential transactions when policies are kept private.