User Tools

Site Tools


projects_list

This is an old revision of the document!


Partial List of Projects Offered

Title: Graphical Simulator for Systems Specified using Communicating Concurrent Kleene Algebra Supervisor: Dr. Jason Jaskolka

	jaskolka@sce.carleton.ca
	(613) 520-2600 Ext. 1873
       

Project Description Simulating the behaviour and operation of a system provides a means for studying the dynamics and evolution of the system, and can aid in verifying and validating that the system behaves as expected under different scenarios and alternative system conditions. This can help to ensure that any potential issues leading to unsafe or insecure system behaviours can be addressed while at the system specification and design stages. Communicating Concurrent Kleene Algebra (C²KA) [1] is an algebraic framework for specifying distributed multi-agent systems. It offers a hybrid view of communication and concurrency that encompasses the characteristics of both state-based and event-based models.

Although C²KA offers facilities to study the behaviour of distributed systems at a convenient abstract algebraic level, it currently lacks a means for directly simulating and displaying the behaviour of a system specified using its algebraic framework. To address this need, this project aims to develop a graphical simulation tool that allows for the visualization of the step-wise simulation (at both the event and state levels) of small systems (or sub-systems) specified using C²KA. It will involve the development of the requirements, architectural and detailed design, and implementation of a practical and scalable software tool to aid in the analysis of distributed multi-agent systems.

Additional Comments: • Strong programming skills are essential • Familiarity and/or experience with programming GUIs and graphing libraries is recommended • Thorough knowledge of Mealy automata or finite state machines is recommended

References: [1] J. Jaskolka, R. Khedri, and Q. Zhang. “Endowing concurrent Kleene algebra with communication actions.” In P. Höfner, P. Jipsen, W. Kahl, and M.E. Müller, editors, Proceedings of the 14th International Conference on Relational and Algebraic Methods in Computer Science, volume 8428 of Lecture Notes in Computer Science, pages 19-36. Springer International Publishing Switzerland, Marienstatt, Germany, April 2014


Title: Tool Support for Extracting Intended System Interactions from UML Diagrams

Supervisor: Dr. Jason Jaskolka

	jaskolka@sce.carleton.ca
	(613) 520-2600 Ext. 1873

Project Description: Systems typically have intended sequences of communication and interactions among their constituent components to co-ordinate their behaviours when performing their functions. Often, this set of intended system interactions is provided by the system designer in the form of UML diagrams (e.g., collaboration diagrams, sequence diagrams, message passing diagrams, etc.).

Currently, the extraction of intended system interactions from system designs is a manual, labour-intensive, and error-prone process. This project aims to address these issues by automating the extraction process. The goal of this project is to develop a practical and scalable software tool that can extract a set of intended system interactions (as described in [1]) from a representation of a system design as a UML diagram. It will involve the development of the requirements, architectural and detailed design, and implementation of the tool.

The resulting set of intended system interactions is expected to serve as a reference set of system interactions to aid in identifying implicit component interactions (i.e., those interactions that may be unexpected or unforeseen by the system designers). In the long term, the tool support developed in this project will be incorporated into larger workflows aiming to identify and analyze implicit component interactions in complex distributed systems, ultimately impacting the security and safety of a system.

Additional Comments: • Strong programming skills are essential • Familiarity with UML is highly recommended

References: [1] J. Jaskolka and J. Villasenor. “An approach for identifying and analyzing implicit interactions in distributed systems.” IEEE Transactions on Reliability, 66(2):529-546, June 2017.


Title: Automated Theorem Proving for Distributed System Cybersecurity

Supervisor: Dr. Jason Jaskolka

     		jaskolka@sce.carleton.ca
	(613) 520-2600 Ext. 1873

Project Description: Distributed systems consisting of numerous interacting software and/or hardware components are commonplace in many of todayÕs critical systems, including critical infrastructures, industrial control systems, automobiles, and airplanes. The ability to identify, analyze and mitigate cybersecurity vulnerabilities in large and complex distributed systems remains among the top priorities for governments and service providers.

Recent research has investigated the identification and analysis of cybersecurity threats and vulnerabilities in distributed systems specified using an algebraic modelling framework called Communicating Concurrent Kleene Algebra (C2KA) [1]. In this project we seek to implement the algebraic theory of Communicating Concurrent Kleene Algebra (C2KA) for use with a proof assistant (e.g., Isabelle/HOL, Coq, etc.) or automated theorem prover (e.g., Prover9, SPASS, etc.). The objective of this research project is to provide support for the verification of theoretical results regarding the specifications of distributed system specified using C2KA. Such results can then be used to develop approaches for identifying, analyzing, and mitigating cybersecurity vulnerabilities in such systems.

In the current research, proofs that systems specified using C2KA have desirable cybersecurity properties are done using pencil-and-paper. However, the proofs often become complex and challenging, and thus, the process lacks efficiency and is prone to errors. The development of adequate tool support can simplify this process and enable results to be obtained more quickly and easily.

This project provides an excellent opportunity for students to explore the use of state-of-the-art tools and technologies for specifying and verifying distributed multi-agent systems using modern algebraic specification frameworks. It will allow students to gain experience in adopting formal methods for ensuring the security of software systems and applications.

Additional Comments: ¥ Strong background in discrete mathematics and algebra is required ¥ Good programming skills are recommended ¥ Interest in automated theorem proving and formal methods for software and systems engineering

References: [1] J. Jaskolka, R. Khedri, and Q. Zhang.ÊEndowing concurrent Kleene algebra with communication actions. In P. Hšfner, P. Jipsen, W. Kahl, and M.E. MŸller, editors,ÊProceedings of the 14th International Conference on Relational and Algebraic Methods in Computer Science, volume 8428 of Lecture Notes in Computer Science, pages 19-36. Springer International Publishing Switzerland, Marienstatt, Germany, April 2014


Title: Identifying and Specifying Security Threats in Architectural Designs

Supervisor: Dr. Jason Jaskolka

     		jaskolka@sce.carleton.ca
	(613) 520-2600 Ext. 1873

Project Description: The proposed project is part of a larger research effort that aims to answer the following research question: Can we show that a software system built using security design patterns is secure? To advance toward answering the research question, the proposed project will focus on identifying, specifying, and detecting security threats targeting the communication channels in the architectural design of distributed software systems. Specifically, this project seeks to identify possible threats and attacks that target vulnerabilities in communication channels in distributed systems. This will provide us with a set of threats (or classes of threats) that will need to be mitigated in such systems. Then, using the Alloy specification language [1], we will aim to specify the identified threats by describing how an attacker would exploit those threats to undermine the security objectives of the system (e.g., eavesdrop on a communication channel to obtain sensitive information, deny system components from communicating at all, etc.).

Additional Comments: • Strong background in discrete mathematics and first-order logic is required • Good programming skills are recommended • Through understanding of software architecture and design is desired

References: [1] Jackson D. (2006). Software Abstractions: Logic, Language, and Analysis. The MIT Press.


Title: Practical GUI testing Supervisor: Prof. Yvan Labiche (labiche@sce.carleton.ca)

Brief Description: As part of the Masters of Engineering degree program, which provides technical expertise at the graduate level, this SYSC5900 course project consists (1) in becoming familiar with a number of software tools that are typically used for testing software with a graphical user interface (GUI) and (2) in experimenting with those tools on at least two GUI-based software. The learning objectives of the project course therefore include (i) knowledge of principles for and issues of testing software that has a GUI, (ii) familiarity with typical software testing tools to conduct GUI-based software, (iii) experimental software engineering (i.e., principles of experimentations in software engineering research).

Comments: The work will be conducted under the supervision of the professor and a Ph.D. candidate. Software construction, i.e., programming (e.g., Java), is a pre-requisite. Knowledge of software testing is *not* a pre-requisite. The project course would ideally take place in the Fall of 2017.


Title: Practical State-Based testing Supervisor: Prof. Yvan Labiche (labiche@sce.carleton.ca)

Brief Description: As part of the Masters of Engineering degree program, which provides technical expertise at the graduate level, this SYSC5900 course project consists (1) in becoming familiar with state-of-the-art techniques to verify (through testing) software implementation from a state machine describing its behaviour (i.e., functional or black-box testing), and (2) in experimenting with these techniques on a number of software systems that exhibit (and are therefore specified with) a state-based behaviour. The learning objectives of the project course therefore include (i) knowledge of principles for and issues of testing software that exhibit state-based behaviour, (ii) expertise with the application of those techniques on real software, (iii) experimental software engineering (i.e., principles of experimentations in software engineering research). Comments: The work will be conducted under the supervision of the professor and a Ph.D. candidate. Software construction, i.e., programming (e.g., Java), is a pre-requisite. Knowledge of software testing is *not* a pre-requisite. The project course would ideally take place in the Fall of 2017.


Title: Practical Test Case Diversity Supervisor: Prof. Yvan Labiche (labiche@sce.carleton.ca)

Brief Description: As part of the Masters of Engineering degree program, which provides technical expertise at the graduate level, this SYSC5900 course project consists (1) in becoming familiar with principles of and issues with software testing, (2) becoming familiar with the principle that high test case diversity is assumed to lead to high fault detection, and (3) automatically measuring test case diversity, using various metrics, of a number of test suites for a number of software under test. The learning objectives of the project course therefore include (i) knowledge of software testing principles, including test case diversity, (ii) software construction of a framework so test case diversity can be measured according to various state-of-the-art diversity metrics (recall a framework is meant to be extended, so software design is an important aspect of the project), (iii) execution of the framework, with implemented state-of-the-art diversity metrics, on several sets of test cases for several software systems under test, and (iv) experimental software engineering (i.e., principles of experimentations in software engineering research).

Comments: The work will be conducted under the supervision of the professor. Software construction, i.e., programming (e.g., Java), is a pre-requisite. Knowledge of software testing is *not* a pre-requisite. The project course can take place either in the Fall of 2017 or Winter (or even Summer) of 2018.


Title: Practical Clone detection in test code Supervisor: Prof. Yvan Labiche (labiche@sce.carleton.ca)

Brief Description: As part of the Masters of Engineering degree program, which provides technical expertise at the graduate level, this SYSC5900 course project consists (1) in becoming familiar with the issues of cloning (e.g., duplications) in test code (also known as test script), (ii) in becoming familiar with state-of-the-art of clone detection techniques, and (iii) automatically detecting clones in test code for freely available test code for open-source software. The learning objectives of the project course therefore include (i) knowledge of software testing principles, (ii) knowledge of clone detection (this applies to test code but also to any piece of application code since we use the same techniques), and (iii) experimental software engineering (i.e., principles of experimentations in software engineering research). Comments: The work will be conducted under the supervision of the professor and a Ph.D. candidate. Software construction, i.e., programming (e.g., Java), is a pre-requisite. Knowledge of software testing is *not* a pre-requisite. The project course can take place either in the Fall of 2017 or Winter (or even Summer) of 2018.


Title: Development of real-time embedded systems using a model-based approach Supervision: Professor Gabriel A. Wainer Gabriel.Wainer@sce.carleton.ca

Description:

Real-time systems are built as sets of components interacting with their environment. In most cases (including robotics, traffic control, manufacturing and industrial applications, etc.), these applications must satisfy “hard” timing constraints. If these constraints are not met, systems decisions (even correctly computed) can lead to catastrophic consequences for goods or lives. The development of real-time controllers in distributed environments has been proven a very complex task, in terms of both development difficulties and related costs. We have provided a new systematic method and associated automated tools to develop hard real-time control applications reducing both development costs and delivery time. We use a simulation-based methodology for development, incrementally replacing simulated components by their real counterparts interacting with the surrounding environment.

This project involves continuing the development of the CD++ Builder platform (the Eclipse-based project begun during the Summer Term 2003). The platform integrates some existing simulation tools (written in Java and C++). The project covers a complete software development cycle starting with requirements definition, followed by design, implementation, testing, and the delivery of a working, documented IDE. The activities will be carried out in the CFI Advanced Laboratory for Real-Time Simulation (ARS). This infrastructure consists of a high-performance computing platform (64 high speed processors linked with a very high speed interconnect) to support an advanced real-time simulation engine (including AD/DA interfaces and graphics workstations for human interaction).

Expected learning opportunities include: • an introduction to modeling and simulation tools • fine tuning C++ skills • fine tuning Java skills • real-time and embedded systems development techniques • experience in an advanced high performance computing environment

http://www.sce.carleton.ca/faculty/wainer/ars


Title: Advanced Visualization for complex simulation models Supervision: Professor Gabriel A. Wainer Gabriel.Wainer@sce.carleton.ca

Description:

Cell-DEVS is a technique that enables defining grid-shaped discrete event models. Very complex systems can be modeled easily thanks to the availability of high level techniques and associated tools. We have recently defined very complex models using Cell-DEVS (ranging from fire spreading, watershed forming, or ant foraging up to analysis of the behavior of the heart tissue).

Different visualization techniques have been applied to the current simulation engines (based on Java and VRML). The goal of this project is to improve 3D visualization techniques based on VRML, XML and Java3D. The goal of this project is to improve the currently existing graphical environment enabling the users to easily visualize the simulation models in 3D worlds. This includes distributed execution via the Internet using a web-based interface. The activities will be carried out in the CFI Advanced Laboratory for Real-Time Simulation (ARS) and Carleton Immersive Media Studio lab (CIMS) This infrastructure consists of a high-performance computing platform (64 high speed processors linked with a very high speed interconnect) to support an advanced real-time simulation engine (including AD/ DA interfaces and graphics workstations for human interaction). It will involve linking the visualization tools available at CIMS with the ARS lab equipment using high speed interconnection networks.

http://www.sce.carleton.ca/faculty/wainer/ars

projects_list.1534774694.txt.gz · Last modified: 2018/08/20 10:18 by gwainer