Bruda.CA - part

msc_theses

Anonymous (anonymous@undisclosed.example.com) — 2025-07-26T12:50:51+00:00

Wed 2 Jul 2025 1:07 pm -0400		current
Line 1:		Line 1:
		+	====== On the Equivalence between Must-Test Specifications and the Linear Temporal Logic ======
		+	By Atefeh Farhadi, July 2025. Full paper: {{ :part:farhadi20250711.pdf \|}}
		+
		+	This paper explores the connections between two formal verification techniques: must testing and Linear Temporal Logic (LTL). Both are vital for validating system behaviors and ensuring proper operation. Must testing captures dynamic behaviors and ensures system requirements are met under all execution scenarios, while LTL specifies and verifies temporal properties within systems. Concretely, we explore the equivalence between must testing and LTL. We develop a practical (algorithmic) framework to translate must-test specifications into equivalent LTL formulas. While we thus go only half-way toward establishing an equivalence, we believe that the conversion the other way around is possible as well. On a practical note, we also note that model checking (the algorithmic LTL verification framework) is a very mature technology widely uses in practice, while must testing is deployed to a much lesser extent. We therefore argue that our conversion is much more useful for practical applications. This being said, a conversion of LTL formulae into equivalent must tests is a necessary future expansion of this study to establish formally the equivalence of the two frameworks.
		+
	====== On TorXakis Correctness as an ioco Implementation: An Empirical Model-Based Evaluation ======		====== On TorXakis Correctness as an ioco Implementation: An Empirical Model-Based Evaluation ======
	By Reza Ghasemi, May 2025. Full paper: {{ :part:ghasemi202505.pdf \|}}		By Reza Ghasemi, May 2025. Full paper: {{ :part:ghasemi202505.pdf \|}}

part_members

Anonymous (anonymous@undisclosed.example.com) — 2021-11-08T21:53:42+00:00

Thu 13 Aug 2020 3:52 pm -0400		current
Line 5:		Line 5:
	====== Members ======		====== Members ======

		+	* Movahed Abdolahi
		+	* Afshin Bahrampour
		+	* Ali Irannezhadi
	* Simin Li < <li@cs.ubishops.ca> >		* Simin Li < <li@cs.ubishops.ca> >
-	* Javad Omidvar < <omidvar@cs.ubishops.ca> >	+	* Shahin Novin

	====== Alumni ======		====== Alumni ======

		+	* Javad Omidvar (MSc, 2021) < <omidvar@cs.ubishops.ca> >
	* Tianqi Xiao (MSc, 2020) < <xiao@cs.ubishops.ca> >		* Tianqi Xiao (MSc, 2020) < <xiao@cs.ubishops.ca> >
	* Mehrdad Naserdoust (MSc, 2020) < <naserdoust@cs.ubishops.ca> >		* Mehrdad Naserdoust (MSc, 2020) < <naserdoust@cs.ubishops.ca> >

part

Anonymous (anonymous@undisclosed.example.com) — 2014-11-30T20:37:36+00:00

Wed 16 May 2012 10:44 am -0400		current
Line 2:		Line 2:
	Our research interests encompass all the aspects of parallel computations, including distributed systems. We are also interested in real-time computations. Unsurprising, our main focus is therefore at the intersection of these two areas, that is, in the domain of parallel and distributed real-time computations.		Our research interests encompass all the aspects of parallel computations, including distributed systems. We are also interested in real-time computations. Unsurprising, our main focus is therefore at the intersection of these two areas, that is, in the domain of parallel and distributed real-time computations.

-	We approach the mentioned areas from three perspectives: complexity-theoretic, formal methods and testing, and systems. Our main drive is currently on formal methods and conformance testing, but we are also involved in complexity-theoretic approaches and to some degree in systems.	+	We approach the mentioned areas from three perspectives: complexity-theoretic, formal methods and testing, and systems. Currently our main drive is in the former area, namely in formal language models of parallel computations. We are investigating several such models in the family of parallel communicating grammar systems, with research into corresponding automata being considered.

-	In a first variant of conformance testing (e.g., model checking), the specification consists in a logical formula, which is checked against the implementation; in a second variant (e.g., model-based testing) the specification takes an algebraic form and is then compared with the implementation either directly or via systematic test suites. A mixed, logic and algebraic approach has been tried more or less incipiently in the area of untimed (non-real-time) systems. One of the research directions we are pursuing is such a unified approach for real time. In particular, a hybrid approach to real-time specification should become possible: we will allow logic specifications for those parts of the system most suitable for such, and algebraic specifications for those parts which are more suitable for such a description.	+	At the same time we are active in formal methods. Conformance testing is mostly focused on finite-state systems and is thus suitable for the verification of hardware and communication protocols, and less suitable for the verification of complex software. Conformance testing of infinite systems—more suitable for software verification—has received however sustained attention recently, though most of this attention is on the logical (model checking) side. Another direction in our research is thus the study of algebraic, compositional approaches to this area. This research is based on visibly pushdown languages as well as grammar systems. Our work on the matter is not real time, but we plan to extend it into the real-time domain in the near future.

-	Conformance testing is mostly focused on finite-state systems and is thus suitable for the verification of hardware and communication protocols, and less suitable for the verification of software. Conformance testing of infinite systems—more suitable for software verification—has received however sustained attention recently, though most of this attention is on the logical (model checking) side. Another direction in our research is the study of algebraic, compositional approaches to this area. Our work on the matter is not real time, but we plan to extend it into the real-time domain soon. Our work on the matter is based on visibly pushdown languages, but plans to extend it to context-free constructs and beyond exist.	+	We are also interested in the complexity theory of massively parallel systems. Recent, continuing work on the matter includes the characterization of models with reconfigurable busses as opposed to models with shared memory.

-	In all, we are investigating more or less in parallel algebraic approached to the conformance testing of infinite-state systems, and also unified approaches (logic and algebraic) of classical (finite-state) systems. One day these will be joined together into a nice unified theory of conformance testing for infinite-state systems.	+	Some research in the systems area exists, though this is currently on the back burner (but will increase in importance as soon as the supporting theoretical work is completed).
-		+
-	We are also interested in the complexity theory of massively parallel systems. Recent, continuing work on the matter includes the characterization of models with reconfigurable busses as opposed to models with shared memory.	+

publications

Anonymous (anonymous@undisclosed.example.com) — 2024-02-07T15:26:13+00:00

Sun 6 Nov 2022 12:21 pm -0500		current
Line 8:		Line 8:

	====== Journal papers ======		====== Journal papers ======
		+	- O. N. Timo, T. Xiao, F. Avellaneda, Y. Malik, and S. Bruda, __Evaluating trustworthiness of decision tree learning algorithms based on equivalence checking__, AI and Ethics (2024), [[https://doi.org/10.1007/s43681-023-00415-0]].
	- C. Huang and S. D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C12-2/info12-2-2.pdf\|Improved balance in multiplayer online battle arena games]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 12:2 (2020) 183-204.		- C. Huang and S. D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C12-2/info12-2-2.pdf\|Improved balance in multiplayer online battle arena games]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 12:2 (2020) 183-204.
	- Mary Sarah Ruth Wilkin and Stefan D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C8-2/info82-01.pdf\|Parallel communicating grammar systems with context-free components are Turing complete for any communication model]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 8:2 (2016), 113−170.		- Mary Sarah Ruth Wilkin and Stefan D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C8-2/info82-01.pdf\|Parallel communicating grammar systems with context-free components are Turing complete for any communication model]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 8:2 (2016), 113−170.

recruitment

Anonymous (anonymous@undisclosed.example.com) — 2015-05-03T21:19:56+00:00

Sat 25 Apr 2026 11:23 am -0400	current
Line 1:	Line 1:
	+	Stefan Bruda is supervising a team of MSc students working in a [[https://part.bruda.ca\|number of areas]] and he is interested in expanding his team. We welcome graduate students interested in working on real-time systems from three perspectives: complexity-theoretic, formal methods and testing, and systems.
	+
	+	Note however that the later perspective (systems) is currently on the backburner; no involvment is taking place or expected in the near future.
	+
	+	We welcome qualified students interested on the matter and we shall then discuss the concrete topic of research for the programme. The ideal candidate comes from either Computer Science of Math, has a solid background in discrete math, and is interested in one of the following areas: formal methods, formal languages, automata, complexity theory.
	+
	+	While experience in the above mentioned areas is a plus, candidates should not feel discouraged by lack of such background. Indeed, the Department of Computer Science at Bishop's University offers a good selection of graduate courses on these topics. We are also a friendly team and we support each other. Interest on the matter and hard work have been (and will continue to be) keys to success in our group.
	+