User Tools

Site Tools


projects_list

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Last revision Both sides next revision
projects_list [2017/09/01 15:12]
gwainer
projects_list [2018/10/05 08:24]
gwainer
Line 1: Line 1:
 ====== Partial List of Projects Offered ====== ====== Partial List of Projects Offered ======
- 
  
 **Title: Graphical Simulator for Systems Specified using Communicating Concurrent Kleene Algebra ​ **Title: Graphical Simulator for Systems Specified using Communicating Concurrent Kleene Algebra ​
Line 45: Line 44:
 [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. [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: ​Machine Learning for Medical Imaging** +**Title: ​Identifying and Specifying Security Threats in Architectural Designs**
-Supervisor:​ Prof. Eran Ukwatta+
  
-Brief description+Supervisor: Dr. Jason Jaskolka 
-Atherosclerosis is a silent disease, where vulnerable plaques develop in the medium and large sized arteriesThe patients with the advanced atherosclerotic disease may suffer major cardiovascular events, such as heart disease or stroke with no overt symptoms ​Traditional imaging approaches, such as computed tomography angiography ​(CTA), provide little soft tissue contrast and/or no cross-sectional viewsNew developments in engineering and the physics behind magnetic resonance imaging (MRI) have created ​the potential for non-invasive ​and in vivo measurements of atherosclerosis for the assessment ​of plaque burdenMRI imaging techniques not only provide cross-sectional views of the vessel wallbut also the soft tissue contrast good enough ​to distinguish vulnerable soft plaque from low-risk calcified plaqueCarotid arteries are major site for atherosclerotic plaque development. One of the major steps in the clinical workflow in obtaining quantitative information about the plaque composition is the segmentation ​of the vessel wall of the carotid arteriesHowever, manual segmentation of the vessel wall is tedious and subject to high inter-observer variabilityThere is, therefore, a need for the development of automated methods that will increase the precisionaccuracyconsistency ​and efficiency ​of segmentationIn the proposed research projectthe student will develop ​and evaluate a new image processing technique for segmentation of the vessel wall of the carotid arteries for the assessment of atherosclerotic disease in humans.+       jaskolka@sce.carleton.ca 
 + (613520-2600 Ext1873 
 + 
 +          
 +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 systemsSpecificallythis project seeks to identify possible threats and attacks that target vulnerabilities in communication channels in distributed systemsThis will provide us with 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 communication channel to obtain sensitive informationdeny system components from communicating at alletc.). 
 + 
 +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: How to use medical imaging to diagnose and monitor patients at risk of heart attack?** 
-Supervisor:​ Prof. Eran Ukwatta 
  
-Brief descriptionMyocardial infarction or a heart attacka medical condition ​in which regions ​of a patient'​myocardium lose viability due to prolonged ischemiais prominent cause of serious complications,​ including heart failure ​an ventricular arrhythmiaPrevious studies have demonstrated ​that infarct region plays an important role in creating ​the abnormal +**Project TitleTooling infrastructure to compute test diversity in state-based testing \\ 
-electrical activity ​of the heartA T1 mapping techniquenamely ​the multi-contrast late gadolinium enhanced ​(MCLEimaginghave recently shown to be more reproducible in quantifying infarct volumes ​than the conventional late gadolinium enhanced cardiac magnetic resonance ​(LGE-CMRtechniqueFurther, a recent study has shown that infarct volumes extracted from MCLE images were more sensitive ​in predicting patient ​outcomes ​than those extracted ​from conventional LGE-CMR images.+ 
 +Supervisor:​** Yvan Labiche (yvan.labiche@carleton.ca) 
 + 
 +Description:​ There is some empirical evidence that when test cases are created as diverse as possiblethey are more effective at revealing faults. There are however many different ways to define and compute diversity of tests. Some measures of test diversity come from information theory, such as the Levenshtein distance. Other measures of diversity can be borrowed from biology (i.e., diversity ​in a population). It is unclear what measure(s) ​of diversity make sense when computing diversity of test cases in test suite (set of test cases). To precisely determine what measure(s) make(s) sensewe need to perform experiments on large sample ​of test cases (that can involve hundred of thousands of tests to compare). This cannot be made by hand an automation is necessaryThis project is to create a software tool infrastructure ​that will allow the definition and implementation of various test diversity metrics and their use of real test cases and test suites. The infrastructure will have to be modular to facilitate the definition of new diversity metrics ​in the future, accommodate new tests and test suites to measure. Although initially designed to work on state based tests, the infrastructure should accommodate other kinds of tests in the future. The infrastructure therefore will resemble a framework and will extensively rely on design patterns. 
 +Additional comments: requires competency in programming,​ especially Java; requires knowledge ​of software design principles and design patterns. 
 +Expected learning outcomes: increased expertise in software design, in framework construction,​ in software programming 
 + 
 + 
 +---- 
 + 
 +**Project Title: Suggest you own idea for the interactive SWall project\\ 
 + 
 +Supervisor: ** Yvan Labiche (yvan.labiche@carleton.ca) 
 + 
 +Description:​ The SWall project (http://​sce.carleton.ca/​swall/​) is a wall of touch screens between Mackenzie blocks 3 and 4 on the 4th floor. The wall is also equipped with a cameraand can accommodate other devises. The SWall already have some Apps; feel free to try them. You are encouraged to suggest new ideas of App, fun, educational or other, that can be created, installed and run on the SWall.  
 +Additional comments: requires programming competency; requires fun ideas. 
 +Expected learning outcomes: increased expertise in software design and programming 
 + 
 + 
 +---- 
 + 
 +**Project Title: Software interface to Satisfiability Modulo Theory ​(SMTsolvers\\ 
 + 
 +Supervisor: ** Yvan Labiche (yvan.labiche@carleton.ca) 
 + 
 +Description:​ Satisfiability Modulo Theory (SMT) solvers are software programs that automatically solve decision problems that are expressed as logical formula with respect to differentsometimes combined, theories. A simple example is a logical formula that uses the first-order logic theory; in other words, Boolean formulas. There are more complex theories that are difficult ​to handle automatically by a computer program, such as Real numbers, Integers, Lists, Arrays, Bit Vectors or Strings. An SMT solver mixing several theories can be asked to solve a decision problem defined as follows: find values for integer variable I, string variable S and character variable C such that S has at least 3 characters but no more than 15, C is an alpha-numerical that appears I times in S. Of course, such a problem must be specified with a language that can be processed by the SMT solver. A number of SMT solvers exist, including Yices (http://​yices.csl.sri.com/​),​ Microsoft’s Z3 (https://​github.com/​Z3Prover/​z3). Such solvers need to be integrated into a prototype Java software developed at Carleton University. The purpose of this project is to study typical SMT solvers, how they can be integrated into that other Java software, suggest a software design solution to then implement this integration. 
 +Additional comments: requires programming proficiency 
 + 
 +Expected learning outcomes: increased software design and programming,​ introduction to SMT solvers 
 + 
 + 
 +---- 
 + 
 +**Project Title: Studying structural complexity of test code and application code\\ 
 + 
 +Supervisor: **Yvan Labiche (yvan.labiche@carleton.ca) 
 + 
 +Description:​ Software metrics are typically used in industry and research to evaluate software productsBy using measures of source code, one can estimate fault-proneness,​ understandability,​ foreseeable reliability … Some metrics are easy to compute, such as the number of lines of code, a.k.a. LOC (though not counting blank lines or comments), the number of lines of comments, the number of classes (in object-oriented programs), the number of functions/​methods. Some metrics are more complex to use and require tool support, such as McCabe’s cyclomatic complexity ​that measures the number of linearly independent paths in a piece of code. There is an ongoing debate as to whether the more complex metrics (e.g., cyclomatic complexity) are linearly dependent on simpler ones (e.g., LOC): if this is indeed the case, then one might as well use the simpler ones. There is also an unknown: is code created to test software more or less complex than the application logic code the test code tests? Mixing the two issues together, are complex metrics linearly dependent on simpler ones when measuring test code. This project will use complexity data from open source software and possibly some industry software to answer these questions. 
 +Additional comments: requires proficiency ​in descriptive and inferential statistics 
 + 
 +Expected learning ​outcomes: Significant knowledge in software measurement techniques 
 + 
 +---- 
 + 
 +**Project Title: Optical hand-held probe for skin cancer\\ 
 + 
 +Supervisor: **Sreeraman Rajan (sreeramanr@sce.carleton.ca) 
 + 
 +Description:​  
 +The goal of this project is to develop a hand-held probe for detecting skin cancer using nonlinear optical imaging. This probe will use a high power femtosecond laser to scan the skin surface using a MEMS mirror. The student will be involved in developing an FPGA-based image acquisition system for this probe. 
 + 
 +Please contact Dr. Murugkar (http://​people.physics.carleton.ca/​~smurugkar/​) in the Department of Physics at Carleton University to be a part of this exciting research in biophotonics. Dr. Sreeraman Rajan from Systems and Computer Engineering will be cosupervising this project. 
 + 
 +Needed background: ​ Knowledge of FPGA, image processing and signal processing fundamentals,​ good knowledge of electronics,​ embedded design. 
 + 
 +Biomedical specialty is not a must. Having the ability to design circuits and use FPGA is essential. 
 + 
 +---- 
 + 
 +**Title: Development of real-time embedded systems using a model-based approach**  
 + 
 +Supervisor:​ 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)
  
-Recently, computational modeling of hearts has emerged as a promising tool to guide patient-specific diagnosis ​and the treatment of associated rhythm disordersHowever, ​to accurately represent patient-specific structural remodelingcomputational models must incorporate accurate geometric reconstructions of infarct regionsGiven that the infarct regions extracted from MCLE images are more accurate than the ones extracted from conventional LGE-CMR images, ​the personalized ​models ​built using infarct regions extracted from MCLE images may provide more sensitive ​in predicting abnormal electrical activity of the heart. The objective ​of this +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 VRMLXML and Java3DThe 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.
-study is to test this hypothesis.+
  
 +http://​www.sce.carleton.ca/​faculty/​wainer/​ars
  
projects_list.txt · Last modified: 2019/12/07 16:52 by gwainer