{"id":817,"date":"2022-05-09T15:21:40","date_gmt":"2022-05-09T15:21:40","guid":{"rendered":"https:\/\/carleton.ca\/ericsson\/?p=817"},"modified":"2025-04-14T11:29:40","modified_gmt":"2025-04-14T15:29:40","slug":"ericsson-fellow-and-grad-student-james-baak-has-a-passion-for-formal-methods","status":"publish","type":"post","link":"https:\/\/carleton.ca\/ericsson\/2022\/ericsson-fellow-and-grad-student-james-baak-has-a-passion-for-formal-methods\/","title":{"rendered":"Ericsson Fellow and Grad Student James Baak has a Passion for Formal Methods"},"content":{"rendered":"\n
\n
\n\n
\n
\n
\n

\n Ericsson Fellow and Grad Student James Baak has a Passion for Formal Methods\n <\/h1>\n \n \n <\/header>\n\n <\/div>\n\n <\/div>\n\n <\/div>\n<\/section>\n\n\n\n\n\n

By Ellen Tsaprailis
Photos By Lindsay Ralph<\/em><\/p>\n\n\n\n

James Baak<\/a> is one of six graduate students who are Ericsson Fellows<\/a> at Carleton University\u2014a unique, talent-building program born out of the Ericsson-Carleton University Partnership for Research and Leadership in Wireless Networks<\/a>.<\/p>\n\n\n\n

Instead of working as a teaching assistant during their graduate studies, Baak and the other fellows are being supported to fully focus on their pioneering wireless communications research and get input from both their academic supervisors and Ericsson professionals.<\/p>\n\n\n\n

For Baak, his research specialty is diving into automating formal methods.<\/p>\n\n\n

\n

\u201cI want to bridge the gap between the average designer\/developer and have an automated process to introduce them to formal methods,\u201d says Baak of his long-term research goal.<\/p><\/blockquote>\n<\/div>\n\n\n

\"\"
James Baak is an Ericsson Fellow and Master of Applied Science Student<\/figcaption><\/figure>\n\n\n\n

Baak has a Bachelor of Engineering from Carleton, and during his undergrad did a series of co-ops that included government and private industry which provided him relevant work experience and an initial plan to pursue employment after graduating.<\/p>\n\n\n\n

His academic trajectory took a turn when Baak registered for a security engineering course run by Systems and Computer Engineering<\/a> Assistant Professor Jason Jaskolka<\/a> in his final year.<\/p>\n\n\n

\n

\u201cWithout the intention of going to my master\u2019s, Professor Jaskolka and I aligned on some of our views of the use of formal methods in computer systems engineering,\u201d says Baak. \u201cI was quite interested in defining a fully-automated process or formal method to use mathematics or other rigorous notation methods to define, verify and validate systems.\u201d<\/p><\/blockquote>\n<\/div>\n\n\n

Soon after, Baak was invited to start working in Carleton\u2019s Cyber Security Evaluation and Assurance (CyberSEA) Research Lab<\/a>  run by Jaskolka who also agreed to be Baak\u2019s academic supervisor for his fellowship. <\/p>\n\n\n\n

\u201cJames is a valued member of the CyberSEA Research Lab and it\u2019s a pleasure to supervise his research,\u201d says Jaskolka. \u201cJames is developing an approach for reusing formally verified components to address security concerns in the design and development of 5G systems. Through engagement opportunities offered by the Ericsson Fellowship, James has been able to understand the real needs of Ericsson so that his work can be applied in practice. James\u2019 progress to-date has been met with interest by Ericsson, specifically in its potential to help reduce the time and effort required to design and verify critical systems and networks.\u201d<\/p>\n\n\n\n

Using the Alloy language system, Baak is applying his idea of compositional component-based design to ensure safety in 5G systems.<\/p>\n\n\n\n

\u201cWhen we think of components in software engineering, it’s kind of like this independently deployable piece of code that you can put anywhere. What I’m interested in is bringing those components together and connecting them in a way that we can divide and conquer the verification process,\u201d explains Baak. <\/p>\n\n\n\n

\u201cUsually in the types of systems using formal methods it is a mathematical notation of all these components brought together, but it is large and when we give it to a computer or even a human to analyze, it becomes very difficult and complex to go through it and verify that the system is functioning the way it should. So, the goal with my research is to be able to divide up the verification process by defining abstract boundaries around groups of components.\u201d<\/p>\n\n\n\n

Breaking up the verification process into groupings instead of the whole system would be faster and easier to keep components secure.<\/p>\n\n\n\n

\u201cFor example, a web browser client and website server are two separate components of a distributed system which communicate with each other to provide a service to a client,\u201d explains Baak. \u201cThe web browser and the server can be further broken down into their sub-component groups to provide the different functionality of the client or server. The verification of the components can then be verified individually or in their groups.\u00a0Logically, we should be able to say these things can be developed and verified independently as long as certain assumptions and constraints are held true between components when we connect them.\u201d<\/p>\n\n\n\n

\"\"
James Baak<\/figcaption><\/figure>\n\n\n\n

An Ericsson Fellow since Sept. 2020, Baak is in his second year of a master\u2019s of applied science in electrical and computer engineering degree and plans to graduate this summer. Throughout this second year, Baak has been able to devote all his time to his thesis and 5G research.<\/p>\n\n\n\n

Baak\u2019s goal after completing his master\u2019s is to pursue employment in the private sector, perhaps with Ericsson, and is hoping to continue this particular research.<\/p>\n\n\n

\n

\u201cI’m quite interested in this type of methodology,\u201d says Baak. \u201cI would be very interested to try implementing it in the actual industry. It’s very easy to talk about in academia and show some examples on smaller systems, but it’s another thing to actually go into the industry and apply it.\u201d<\/p><\/blockquote>\n<\/div>\n\n\n

Ericsson Fellowship<\/strong>
In this prestigious fellowship program<\/a>, Carleton graduate students conduct hands-on research alongside Ericsson experts in state-of-the-art facilities, ensuring students build skills that are in high demand in today’s telecommunications industry.
<\/p>\n\n\n\n

\"\"<\/figure>\n","protected":false},"excerpt":{"rendered":"

By Ellen Tsaprailis Photos By Lindsay Ralph James Baak is one of six graduate students who are Ericsson Fellows at Carleton University\u2014a unique, talent-building program born out of the Ericsson-Carleton University Partnership for Research and Leadership in Wireless Networks. Instead of working as a teaching assistant during their graduate studies, Baak and the other fellows […]<\/p>\n","protected":false},"author":2,"featured_media":824,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":"","_links_to":"","_links_to_target":""},"categories":[32],"tags":[],"class_list":["post-817","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-news"],"acf":{"cu_post_thumbnail":false},"_links":{"self":[{"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/posts\/817","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/comments?post=817"}],"version-history":[{"count":5,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/posts\/817\/revisions"}],"predecessor-version":[{"id":829,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/posts\/817\/revisions\/829"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/media\/824"}],"wp:attachment":[{"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/media?parent=817"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/categories?post=817"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/carleton.ca\/ericsson\/wp-json\/wp\/v2\/tags?post=817"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}