Communicating Multi-Stack Visibly Pushdown Processes by Davidson Madudu (20 March at 1:30 pm in Johnson 102)

Visibly Pushdown Languages (VPLs) were proposed as a formalism to model and verify concurrent and recursive systems. However, the lack of closure under shuffle for VPLs makes them unsuitable for the specification and verification of such complex systems. On the other hand, Multi-stack Visibly Pushdown Languages (MvPLs) appear to give a more realistic expression of concurrency and recursion in computational systems. Unfortunately, they have a similar limitation to VPL, as they also lack closure under shuffle. However, by relaxing the rigid restrictions placed on the input alphabet of MvPLs in its original definition, and by introducing a natural renaming process, we get closure under shuffle and still retain all existing closure properties. With this result in mind, we propose an MvPL-based compositional specification and verification for complex computational systems.

Bitcoin-Based Decentralized Carbon Emissions Trading Infrastructure Model by Davor Svetinovic (26 February at 2 pm in the Cleghorn Room)

This talk presents a system-of-systems architecture model for a Decentralized Carbon Emissions Trading Infrastructure (D-CETI) with focus on privacy and system security goals. The structure and behavior are implemented as a solution to the problem of trading carbon emissions anonymously among the trading agents. Privacy and security of the trading agents and their carbon credits are the main requirements behind the architecture of D-CETI. The decentralized structure of multiple systems and distributed behavior are the two main features of D-CETI that distinguish it from the traditional carbon trading schemes and protocols. D-CETI is based on Bitcoin, a peer-to-peer digital currency with no central authority, and Open Transactions, a system that simplifies the use of cryptography in financial transactions. The architecture of D-CETI is evaluated and compared with the architecture of five other carbon emissions trading platforms.

Davor Svetinovic is an Associate Professor at Masdar Institute of Science and Technology, UAE. He received his PhD (2006) and MMath (2002) in Computer Science from University of Waterloo, and his BSc (2000) in Computer Science and Mathematics at Bishop's University. Previously, he worked as a visiting researcher at Massachusetts Institute of Technology, and as a postdoctoral researcher at Lero – the Irish Software Engineering Center as well as at the Vienna University of Technology. His current research interests include: software engineering, strategic requirements engineering, systems architecture with emphasis on smart grids, and sustainable development from the systems security perspective.

After his presentation Dr. Svetinovic will hold an informational session on graduate studies and research opportunities at the Masdar Institute of Science and Technology.

Thesis Defense Friday, 31 October at 2 pm in Johnson 102: Parallel Communicating Grammar Systems with Context-Free Components Are Really Turing Complete

Open MSc thesis defense by Mary Sarah Ruth Wilkin. All are welcome.

Parallel Communicating Grammar Systems (PCGS) were introduced as a language-theoretic treatment of concurrent systems. A PCGS extends the concept of a grammar to a structure that consists of several grammars working in parallel, communicating with each other, and so contributing to the generation of strings.

PCGS are generally more powerful than a single grammar of the same type. PCGS with context-free components (CF-PCGS) in particular were shown to be Turing complete. However, this result holds only when a non-standard mean of communication (which we call broadcast communication) is used. We expand the original construction that showed Turing completeness so that broadcast communication is eliminated at the expense of introducing a significant number of additional, helper component grammars. We thus show that CF-PCGS in their original definition are indeed Turing complete. We introduce in the process several techniques that may be usable in other constructions and may be capable of eliminating broadcast communication in general.

We also show how an earlier result proving that CF-PCGS only generate context-sensitive languages is incorrect. We discover that this proof relies of coverability trees for CF-PCGS, but that such coverability trees do not contain enough information to support the proof. We are also able to conclude that coverability trees are not really useful in any pursuit other than the one already considered in the paper that introduces them (namely, determining the decidability of certain decision problems over PCGS).

Undergraduate Capstone Open Source Projects

If you are interested in getting real experience building a substantial software system as part of a distributed team, you'll be interested in UCOSP!

UCOSP is a senior undergraduate course, which has been running since September 2008. In this course, teams of students from several schools work together on an open-source software project. Each student registers in the appropriate course at his or her home institution (in our case this course would be either CS 404 or CS 408) and works in tandem with their peers from across the country. During one intensive weekend early in the course, students travel to meet face-to-face and work together.

This course exposes students to the tools, working practices, and issues that are now routine in global software development. Just as importantly, it enables them to get to know their peers from across the country. UCOSP is sponsored by Canadian CS Department Chairs and several industrial partners.

If you are interested in being involved, please contact Dr. Stefan D Bruda, who is the faculty partner for UCOSP at Bishop's.