To complement previous research on the top-down inclusion of ethics training within engineering programs, this Innovative Practice Work in Progress paper describes a supplementary strategy acknowledging and supporting ethics training as a shared responsibility. As science and technology have ethical impact, accreditation bodies have in the past decades mandated the inclusion of ethics in STEM education. However, the implementation of ethics education is fraught with obstacles. Through a case study of a Faculty-wide effort to support shared responsibility for ethics training, the pros and cons of an institutionally embedded ethics approach are discussed. It is argued that such an approach can provide a rooted base that can also serve to comply with more formal ethics evaluations, by strengthening a view of ethics as craft, acknowledging subject teachers as ethics ambassadors, reforming the hidden curriculum, and depoliticizing institutional politics.

Students in engineering are well trained in solving specified problems, but some have trouble when given problems where there is more than one solution. In their professional life they are much more often confronted with open-ended problems, where there may be more than one solution, and where there may be many ways to reach each one. The goals may be vague, the problem may be underspecified, and the fresh graduate frustrated by the new situation. We present a structured approach to training students in open-ended problem solving. We have introduced a half-day workshop to help students learn to work with open-ended, ill-structured problems, using a different approach than they would for the well-structured problems they are used to. Our results indicate that students have become more creative. Compared to previous years, the students explore more paths towards the goal, and use more elaborate methods. Their approach is similar to that typically used by the best students in previous instances of the course. Students mention creativity and group dynamics as positive aspects of the workshop and the following lab. We conclude that with proper guidance and training, even weaker students can become more creative when solving open-ended problems.

Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.

An engineering graduate needs to master a number of important skills: problem solving, critical thinking, communication, collaboration, etc. In this paper we describe how a course in computer security, taught in the Computer and Information Engineering programme at Uppsala University, has been developed over a period of three years. The aim is to better develop the engineering competencies of students, improving their understanding of course contents, training their ability to reflect on it, and to apply their knowledge when facing realistic problems. The course is designed to activate students, based on practical labs and theoretical tasks which are solved in groups. The student reports are assessed at seminars, where the solutions are presented orally, peer-reviewed and discussed. The seminars encourage and reward activities at the higher levels of taxonomies such as Bloom's. The results of the development, based on a CEQ-based course evaluation, indicate that students take a deeper approach to learning. They develop their problem-solving skills to a high degree, appreciate the practical solving of open-ended problems, and take responsibility for collaborative learning. Their overall satisfaction with the course is quite high, despite indications that they find the workload high.

We propose two strategies to reduce energy consumption for secure data aggregation in wireless sensor networks. While the purpose of data aggregation is to reduce energy consumption, secure data aggregation introduces an overhead making the total energy consumption comparable to naive secure non-aggregation. Another aspect is that the secure data aggregation has higher node congestion than non-aggregation schemes for networks of sizes up to about 100 nodes. Considering a secure data aggregation protocol, our strategies are to reduce the height of the aggregation tree and limit its node degree. The former results in fewer verification messages and a lower total communication load, and the latter reduces node congestion. The most heavily burdened node sends a third of the messages required in the original protocol, which for small networks is lower than with non-aggregation, and the total communication load is lowered compared to non-aggregation.

Psi-calculi extend the pi-calculus with nominal datatypes to represent data, communication channels, and logics for facts and conditions. This general framework admits highly expressive formalisms such as concurrent higher-order constraints and advanced cryptographic primitives. We here establish the theory of weak bisimulation, where the τ actions are unobservable. In comparison to other calculi the presence of assertions poses a significant challenge in the definition of weak bisimulation, and although there appears to be a spectrum of possibilities we show that only a few are reasonable. We demonstrate that the complications mainly stem from psi-calculi where the associated logic does not satisfy weakening. We prove that weak bisimulation equivalence has the expected algebraic properties and that the corresponding observation congruence is preserved by all operators. These proofs have been machine checked in Isabelle. The notion of weak barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for τ actions and preservation of barbs in all static contexts. We prove that weak barbed equivalence coincides with weak bisimulation equivalence.

A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Other proposed extensions of the pi-calculus can be formulated as psi-calculi; examples include the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and a predicate logic for assertions. Our labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic properties of psi-calculi. The proofs have been checked in the interactive proof checker Isabelle. We are the first to formulate a truly compositional labelled operational semantics for calculi of this calibre. Expressiveness and therefore modelling convenience significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.

We present an expressiveness study of linearity and persistence of processes. We choose the ð-calculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the ð-calculus. Each one singles out a natural source of linearity/ persistence also present in other frameworks such as Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing (or proving the non-existence of) encodings among the fragments, a processes-as-formulae interpretation and a reduction from Minsky machines.

We present a concise and natural encoding of the spi-calculus into the more basic /spl pi/-calculus and establish its correctness with respect to a formal notion of testing. This is particularly relevant for security protocols modelled in spi since the tests can be viewed as adversaries. The translation has been implemented in a prototype tool. As a consequence, protocols can be described in the spi calculus and analysed with the emerging flora of tools already available for /spl pi/. The translation also entails a more detailed operational understanding of spi since high level constructs like encryption are encoded in a well known lower level. The formal correctness proof is nontrivial and interesting in its own; so called context bisimulations and new techniques for compositionality make the proof simpler and more concise.

Computer Science has witnessed the emergence of a plethora of different logics, models and paradigms for the description of computation. Yet, the classic Church–Turing thesis may be seen as indicating that all general models of computation are equivalent. Alan Perlis referred to this as the ‘Turing tarpit’, and argued that some of the most crucial distinctions in computing methodology, such as sequential versus parallel, deterministic versus non-deterministic, local versus distributed disappear if all one sees in computation is pure symbol pushing. How can we express formally the difference between these models of computation?

We present a calculus of mobile processes without prefix or summation, called the solos calculus. Using two different encodings, we show that the solos calculus can express both action prefix and guarded summation. One encoding gives a strong correspondence, but uses a match operator; the other yields a slightly weaker correspondence, but uses no additional operators. We also show that the expressive power of the solos calculus is still retained by the sub-calculus where actions carry at most two names. On the other hand, expressiveness is lost in the solos calculus without match and with actions carrying at most one name.

We present the fusion calculus as a significant step towards a canonical calculus of concurrency. It simplifies and extends the /spl pi/-calculus. The fusion calculus contains the polyadic /spl pi/-calculus as a proper subcalculus and thus inherits all its expressive power. The gain is that fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models such as concurrent constraints formalisms. It is also easy to represent the so called strong reduction strategies in the /spl lambda/-calculus, involving reduction under abstraction. In the /spl lambda/-calculus these tasks require elaborate encodings. Our results on the fusion calculus in this paper are the following. We give a structured operational semantics in the traditional style. The novelty lies in a new kind of action, fusion actions for emulating updates of a shared state. We prove that the calculus contains the /spl pi/-calculus as a subcalculus. We define and motivate the bisimulation equivalence and prove a simple characterization of its induced congruence, which is given two versions of a complete axiomatization for finite terms. The expressive power of the calculus is demonstrated by giving a straight-forward encoding of the strong lazy /spl lambda/-calculus, which admits reduction under /spl lambda/ abstraction.