uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 44) Show all publications
Borgström, J., Gutkovas, R., Parrow, J., Victor, B. & Åman Pohjola, J. (2016). A Sorted Semantic Framework for Applied Process Calculi. Logical Methods in Computer Science, 12(1), 1-49, Article ID 8.
Open this publication in new window or tab >>A Sorted Semantic Framework for Applied Process Calculi
Show others...
2016 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 12, no 1, p. 1-49, article id 8Article in journal (Refereed) Published
Abstract [en]

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.

Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can directly represent several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation; the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.

Keywords
Expressiveness, Pattern matching, Type systems, Theorem proving, pi-calculus, Nominal sets
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-262199 (URN)10.2168/LMCS-12(1:8)2016 (DOI)000374769600004 ()
Projects
UPMARC
Funder
Swedish Research Council, 2013-4853
Available from: 2016-03-31 Created: 2015-09-09 Last updated: 2019-02-25Bibliographically approved
Pålsson, S. & Victor, B. (Eds.). (2016). Proceedings från 5:e utvecklingskonferensen för Sveriges ingenjörsutbildningar.
Open this publication in new window or tab >>Proceedings från 5:e utvecklingskonferensen för Sveriges ingenjörsutbildningar
2016 (Swedish)Conference proceedings (editor) (Other academic)
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2016-002
National Category
Computer and Information Sciences Educational Sciences
Identifiers
urn:nbn:se:uu:diva-278929 (URN)
Available from: 2016-02-22 Created: 2016-02-26 Last updated: 2018-01-10Bibliographically approved
Cassel, S. & Victor, B. (2015). A structured approach to training open-ended problem solving. In: Proc. 45th ASEE/IEEE Frontiers in Education Conference: . Paper presented at FIE 2015, October 21–24, El Paso, TX (pp. 417-420). Piscataway, NJ: IEEE Press
Open this publication in new window or tab >>A structured approach to training open-ended problem solving
2015 (English)In: Proc. 45th ASEE/IEEE Frontiers in Education Conference, Piscataway, NJ: IEEE Press, 2015, p. 417-420Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE Press, 2015
Series
Frontiers in Education Conference, ISSN 0190-5848
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-257807 (URN)10.1109/FIE.2015.7344088 (DOI)000371705200073 ()978-1-4799-8453-4 (ISBN)
Conference
FIE 2015, October 21–24, El Paso, TX
Available from: 2015-10-24 Created: 2015-07-08 Last updated: 2018-01-11Bibliographically approved
Borgström, J., Huang, S., Johansson, M., Raabjerg, P., Victor, B., Åman Pohjola, J. & Parrow, J. (2015). Broadcast psi-calculi with an application to wireless protocols. Software and Systems Modeling, 14(1), 201-216
Open this publication in new window or tab >>Broadcast psi-calculi with an application to wireless protocols
Show others...
2015 (English)In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 14, no 1, p. 201-216Article in journal (Refereed) Published
Abstract [en]

Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.

Place, publisher, year, edition, pages
Springer, 2015
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-205258 (URN)10.1007/s10270-013-0375-z (DOI)000349026100012 ()
Projects
UPMARCProFuN
Funder
Swedish Research Council, 2013-4853
Available from: 2013-11-08 Created: 2013-08-15 Last updated: 2018-01-11Bibliographically approved
Cambazoglu, V., Gutkovas, R., Åman Pohjola, J. & Victor, B. (2015). Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support.
Open this publication in new window or tab >>Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support
2015 (English)Report (Other academic)
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2015-033
National Category
Computer Sciences Communication Systems
Research subject
Computer Science with specialization in Computer Communication
Identifiers
urn:nbn:se:uu:diva-268453 (URN)
Projects
ProFuN
Funder
Swedish Foundation for Strategic Research , RIT08-0065
Available from: 2015-12-03 Created: 2015-12-04 Last updated: 2018-01-10Bibliographically approved
Borgström, J., Gutkovas, R., Rodhe, I. & Victor, B. (2015). The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi. ACM Transactions on Embedded Computing Systems, 14(1), Article ID 9.
Open this publication in new window or tab >>The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi
2015 (English)In: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 14, no 1, article id 9Article in journal (Refereed) Published
Abstract [en]

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.

National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-233750 (URN)10.1145/2682570 (DOI)000349302200009 ()
Projects
ProFuNUPMARC
Funder
Swedish Foundation for Strategic Research , RIT08­0065
Available from: 2015-01-21 Created: 2014-10-09 Last updated: 2018-01-11Bibliographically approved
Borgström, J., Gutkovas, R., Parrow, J., Victor, B. & Åman Pohjola, J. (2014). A Sorted Semantic Framework for Applied Process Calculi (extended abstract). In: Trustworthy Global Computing: TGC 2013. Paper presented at 8th International Symposium on Trustworthy Global Computing, August 30-31, 2013, Buenos Aires, Argentina (pp. 103-118). Springer Berlin/Heidelberg
Open this publication in new window or tab >>A Sorted Semantic Framework for Applied Process Calculi (extended abstract)
Show others...
2014 (English)In: Trustworthy Global Computing: TGC 2013, Springer Berlin/Heidelberg, 2014, p. 103-118Conference paper, Published paper (Refereed)
Abstract [en]

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus,  are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.

Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can accommodate several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate  different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Substantial parts of the meta-theory of sorted psi-calculi have been machine-checked using Nominal Isabelle.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8358
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-203382 (URN)10.1007/978-3-319-05119-2_7 (DOI)978-3-319-05118-5 (ISBN)
Conference
8th International Symposium on Trustworthy Global Computing, August 30-31, 2013, Buenos Aires, Argentina
Projects
UPMARCProFuN
Funder
Swedish Foundation for Strategic Research , RIT08­0065
Available from: 2014-03-08 Created: 2013-07-09 Last updated: 2018-01-11
Cassel, S., Nylén, A. & Victor, B. (2014). Enhanced learning by promoting engineering competencies. In: Proc. 44th ASEE/IEEE Frontiers in Education Conference: . Paper presented at FIE 2014, October 22–25, Madrid, Spain (pp. 2044-2049). Piscataway, NJ: IEEE Press
Open this publication in new window or tab >>Enhanced learning by promoting engineering competencies
2014 (English)In: Proc. 44th ASEE/IEEE Frontiers in Education Conference, Piscataway, NJ: IEEE Press, 2014, p. 2044-2049Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE Press, 2014
National Category
Computer Sciences Educational Sciences
Identifiers
urn:nbn:se:uu:diva-232725 (URN)10.1109/FIE.2014.7044328 (DOI)978-1-4799-3921-3 (ISBN)
Conference
FIE 2014, October 22–25, Madrid, Spain
Available from: 2015-02-17 Created: 2014-09-23 Last updated: 2018-01-11Bibliographically approved
Borgström, J., Gutkovas, R., Rodhe, I. & Victor, B. (2013). A Parametric Tool for Applied Process Calculi. In: 13th International Conference on Application of Concurrency to System Design (ACSD 2013): . Paper presented at 13th International Conference on Application of Concurrency to System Design (ACSD), Barcelona, Spain, July 8 - 10, 2013 (pp. 180-185). IEEE Computer Society
Open this publication in new window or tab >>A Parametric Tool for Applied Process Calculi
2013 (English)In: 13th International Conference on Application of Concurrency to System Design (ACSD 2013), IEEE Computer Society, 2013, p. 180-185Conference paper, Published paper (Refereed)
Abstract [en]

High-level formalisms for concurrency are often defined as extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms. Psi-calculi is a parametric framework that can accommodate a wide spectrum of such calculi. It allows the definition of process calculi that extend the pi-calculus with arbitrary data, logic and logical assertions. All such psi calculi inherit machine-checked proofs of the meta-theory such as compositionality and bisimulation congruence.

We present a generic tool for analysing processes from any psi calculus instance, and for implementing new instances with the help of a supporting library. The tool implements symbolic execution and bisimulation algorithms for both unicast and wireless broadcast communication. We illustrate the tool by examples from pi-calculus and the area of wireless sensor networks.

Place, publisher, year, edition, pages
IEEE Computer Society, 2013
Series
International Conference on Application of Concurrency to System Design, ISSN 1550-4808
National Category
Computer Sciences
Research subject
Computing Science
Identifiers
urn:nbn:se:uu:diva-203381 (URN)10.1109/ACSD.2013.22 (DOI)000333827300019 ()978-0-7695-5035-0 (ISBN)
Conference
13th International Conference on Application of Concurrency to System Design (ACSD), Barcelona, Spain, July 8 - 10, 2013
Projects
ProFuNUPMARC
Funder
Swedish Foundation for Strategic Research , RIT08-0065
Available from: 2013-07-09 Created: 2013-07-09 Last updated: 2018-01-11Bibliographically approved
Cassel, S. & Victor, B. (2013). Fördjupat lärande genom aktiverande examination. In: 4:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar: . Paper presented at 4:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar (pp. 51-54).
Open this publication in new window or tab >>Fördjupat lärande genom aktiverande examination
2013 (Swedish)In: 4:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar, 2013, p. 51-54Conference paper, Published paper (Refereed)
National Category
Computer Sciences Educational Sciences
Identifiers
urn:nbn:se:uu:diva-211722 (URN)
Conference
4:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar
Available from: 2013-11-29 Created: 2013-11-29 Last updated: 2018-01-11
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-0174-9032

Search in DiVA

Show all publications