@inproceedings{GuoSekerinski23ParallelOrderBasedCoreMaintenance,
	address = {Salt Lake City, Utah, USA},
	title = {Parallel {Order}-{Based} {Core} {Maintenance} in {Dynamic} {Graphs}},
	url = {https://spaa23.hotcrp.com/paper/92?cap=hcav92YhhYshwFTJRVPCHEPSHNPFgB},
	doi = {10.1145/3605573.3605597},
	abstract = {The core numbers of vertices in a graph are one of the most well-studied cohesive subgraph models because of the linear running time. In practice, many data graphs are dynamic graphs that are continuously changing by inserting or removing edges. The core numbers are updated in dynamic graphs with edge insertions and deletions, which is called core maintenance. When a burst of a large number of inserted or removed edges come in, we have to handle these edges on time to keep up with the data stream. There are two main sequential algorithms for core maintenance, Traversal and Order. The experiments show that the Order algorithm significantly outperforms the Traversal algorithm over a variety of real graphs.

To the best of our knowledge, all existing parallel approaches are based on the Traversal algorithm. These algorithms exploit parallelism only for vertices with different core numbers; they reduce to sequential algorithms when all vertices have the same core numbers. In this paper, we propose a new parallel core maintenance algorithm based on the Order algorithm. Our approach always has parallelism, even for graphs where all vertices have the same core numbers. Extensive experiments are conducted over real-world, temporal, and synthetic graphs on a multicore machine. The results show that for inserting and removing a batch of edges using 16 workers, our method achieves up to 289x and 10x times speedups compared with the most efficient existing method, respectively.},
	booktitle = {International {Conference} on {Parallel} {Processing}, {ICPP} 2023},
	author = {Guo, Bin and Sekerinski, Emil},
	month = aug,
	year = {2023},
	pages = {122--131},
}

The core numbers of vertices in a graph are one of the most well-studied cohesive subgraph models because of the linear running time. In practice, many data graphs are dynamic graphs that are continuously changing by inserting or removing edges. The core numbers are updated in dynamic graphs with edge insertions and deletions, which is called core maintenance. When a burst of a large number of inserted or removed edges come in, we have to handle these edges on time to keep up with the data stream. There are two main sequential algorithms for core maintenance, Traversal and Order. The experiments show that the Order algorithm significantly outperforms the Traversal algorithm over a variety of real graphs. To the best of our knowledge, all existing parallel approaches are based on the Traversal algorithm. These algorithms exploit parallelism only for vertices with different core numbers; they reduce to sequential algorithms when all vertices have the same core numbers. In this paper, we propose a new parallel core maintenance algorithm based on the Order algorithm. Our approach always has parallelism, even for graphs where all vertices have the same core numbers. Extensive experiments are conducted over real-world, temporal, and synthetic graphs on a multicore machine. The results show that for inserting and removing a batch of edges using 16 workers, our method achieves up to 289x and 10x times speedups compared with the most efficient existing method, respectively.

@misc{Sekerinski23TeachingConcurrentProgrammingTalk,
	address = {Online},
	title = {Teaching {Concurrent} {Programming}},
	url = {https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/},
	abstract = {The education in programming has in a certain sense deteriorated since the 80’s and 90’s: programming languages and environments, as common in industry and to which students are exposed in Computer Science, Software Engineering, and related programs, have become complex. Mastering them consumes students to an extent that courses cannot decouple the (timeless) principles of programming from the (short-lived) specifics of the programming environments at hand; the mathematical background on program design is often not taught. This is particularly critical for concurrent programming, which has become increasingly relevant but cannot be mastered without a theoretical background. The author has been developing course material for a required 3rd year Software Engineering course at McMaster University, Concurrent System Design with around 170 students, since 2018 to address that issue by web-based interactive notebooks using Jupyter that combine explanations, the mathematical theory, and execution of programs directly in the notebooks. Correctness reasoning, including non-interference of processes, is explained through hierarchical state diagrams. This talk gives an overview of the course material, which is available as an open educational resource, and reports on the experience.},
	author = {Sekerinski, Emil},
	month = mar,
	year = {2023},
}

The education in programming has in a certain sense deteriorated since the 80’s and 90’s: programming languages and environments, as common in industry and to which students are exposed in Computer Science, Software Engineering, and related programs, have become complex. Mastering them consumes students to an extent that courses cannot decouple the (timeless) principles of programming from the (short-lived) specifics of the programming environments at hand; the mathematical background on program design is often not taught. This is particularly critical for concurrent programming, which has become increasingly relevant but cannot be mastered without a theoretical background. The author has been developing course material for a required 3rd year Software Engineering course at McMaster University, Concurrent System Design with around 170 students, since 2018 to address that issue by web-based interactive notebooks using Jupyter that combine explanations, the mathematical theory, and execution of programs directly in the notebooks. Correctness reasoning, including non-interference of processes, is explained through hierarchical state diagrams. This talk gives an overview of the course material, which is available as an open educational resource, and reports on the experience.

@misc{SekerinskiZhou22ReMoteSlides,
	address = {Hamilton, Ontario, Canada},
	title = {re:mote – {Low}-cost {Software} and {Hardware} {Infrastructure} for {Water} {Quality} {Sensing} in {Indigenous} {Communities}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhou22ReMoteSlides.pdf},
	author = {Sekerinski, Emil and Zhou, Tianyu},
	month = oct,
	year = {2022},
}

@misc{GuoSekerinski22ConcurrentOrderMaintenancePreprint,
	title = {New {Concurrent} {Order} {Maintenance} {Data} {Structure}},
	doi = {10.48550/arXiv.2208.07800},
	abstract = {The Order-Maintenance (OM) data structure maintains a total order list of items for insertions, deletions, and comparisons. 
As a basic data structure, OM has many applications, such as maintaining the topological order, core numbers, and truss in graphs, and maintaining ordered sets in Unified Modeling Language (UML) Specification.
The prevalence of multicore machines suggests parallelizing such a basic data structure. This paper proposes a new parallel OM data structure that supports insertions, deletions, and comparisons in parallel. 
Specifically, parallel insertions and deletions are synchronized by using locks efficiently, which achieve up to 7x and 5.6x speedups with 64 workers.
One big advantage is that the comparisons are lock-free so that they can execute highly in parallel with other insertions and deletions, which achieve up to 34.4x speedups with 64 workers.
Typical real applications maintain order lists that always have a much larger portion of comparisons than insertions and deletions. For example, in core maintenance, the number of comparisons is up to 297 times larger compared with insertions and deletions in certain graphs. 
This is why the lock-free order comparison is a breakthrough in practice.},
	author = {Guo, Bin and Sekerinski, Emil},
	month = aug,
	year = {2022},
	note = {Pages: 11},
}

The Order-Maintenance (OM) data structure maintains a total order list of items for insertions, deletions, and comparisons. As a basic data structure, OM has many applications, such as maintaining the topological order, core numbers, and truss in graphs, and maintaining ordered sets in Unified Modeling Language (UML) Specification. The prevalence of multicore machines suggests parallelizing such a basic data structure. This paper proposes a new parallel OM data structure that supports insertions, deletions, and comparisons in parallel. Specifically, parallel insertions and deletions are synchronized by using locks efficiently, which achieve up to 7x and 5.6x speedups with 64 workers. One big advantage is that the comparisons are lock-free so that they can execute highly in parallel with other insertions and deletions, which achieve up to 34.4x speedups with 64 workers. Typical real applications maintain order lists that always have a much larger portion of comparisons than insertions and deletions. For example, in core maintenance, the number of comparisons is up to 297 times larger compared with insertions and deletions in certain graphs. This is why the lock-free order comparison is a breakthrough in practice.

@book{Sekerinski22SoftwareDesign,
	series = {Open {Library}},
	title = {Interactive {Notebooks} on {Software} {Design}},
	url = {https://vlslibrary.ecampusontario.ca/item-details/#/5772cd52-86a4-4794-977c-13a2257a6e6d},
	abstract = {This is a collection of interactive Jupyter notebooks for teaching software design and, more specifically, concurrent system design on an upper undergraduate level.
(1) Notebooks combine the functionality of a textbook, a programming environment, and slides, thus simplifying the learning experience and allowing students to focus on the essentials. The notebook format allows for more independent study and proves to be suitable for blended learning.
(2) The notebooks use an algorithmic notation for explaining concepts and use Python, Java, and Go for programming.
(3) Program correctness, particularly the notions of loop and class invariants, are introduced alongside the algorithmic notation. State diagrams visualize the correctness conditions, including those for concurrent programs.
(4) An accompanying set of exercise notebooks with programming problems in Python, Java, and Go comes with solutions that can be used as practice material and for semi-automatic grading using the notebook grader extension of Jupyter. The exercises are not part of the public repository but are available on request from the author.
For viewing the notebooks, Jupyter and additional tools need to be installed according to the instructions at https://github.com/emilsekerinski/softwaredesign. The notebooks can also be viewed with JupyterLab. For administering student submissions and for semi-automatic grading, a JupyterHub server is needed. The notebooks can be previewed in HTML form with limitations only.},
	number = {MCMA-990/ID618},
	publisher = {eCampusOntario},
	author = {Sekerinski, Emil},
	month = jun,
	year = {2022},
}

This is a collection of interactive Jupyter notebooks for teaching software design and, more specifically, concurrent system design on an upper undergraduate level. (1) Notebooks combine the functionality of a textbook, a programming environment, and slides, thus simplifying the learning experience and allowing students to focus on the essentials. The notebook format allows for more independent study and proves to be suitable for blended learning. (2) The notebooks use an algorithmic notation for explaining concepts and use Python, Java, and Go for programming. (3) Program correctness, particularly the notions of loop and class invariants, are introduced alongside the algorithmic notation. State diagrams visualize the correctness conditions, including those for concurrent programs. (4) An accompanying set of exercise notebooks with programming problems in Python, Java, and Go comes with solutions that can be used as practice material and for semi-automatic grading using the notebook grader extension of Jupyter. The exercises are not part of the public repository but are available on request from the author. For viewing the notebooks, Jupyter and additional tools need to be installed according to the instructions at https://github.com/emilsekerinski/softwaredesign. The notebooks can also be viewed with JupyterLab. For administering student submissions and for semi-automatic grading, a JupyterHub server is needed. The notebooks can be previewed in HTML form with limitations only.

@article{GuoSekerinski22ParallelGraphTrimming,
	title = {Efficient parallel graph trimming by arc-consistency},
	volume = {78},
	copyright = {2022 The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature},
	issn = {1573-0484},
	url = {https://link.springer.com/article/10.1007/s11227-022-04457-9},
	doi = {10.1007/s11227-022-04457-9},
	abstract = {Given a large data graph, trimming techniques can reduce the search space by removing vertices without outgoing edges. One application is to speed up the parallel decomposition of graphs into strongly connected components (SCC decomposition), which is a fundamental step for analyzing graphs. We observe that graph trimming is essentially a kind of arc-consistency problem, and AC-3, AC-4, and AC-6 are the most relevant arc-consistency algorithms for application to graph trimming. The existing parallel graph trimming methods require worst-case \$\${\textbackslash}mathcal O(nm)\$\$ O ( n m ) time and worst-case \$\${\textbackslash}mathcal O(n)\$\$ O ( n ) space for graphs with n vertices and m edges. We call these parallel AC-3-based as they are much like the AC-3 algorithm. In this work, we propose AC-4-based and AC-6-based trimming methods. That is, AC-4-based trimming has an improved worst-case time of \$\${\textbackslash}mathcal O(n+m)\$\$ O ( n + m ) but requires worst-case space of \$\${\textbackslash}mathcal O(n+m)\$\$ O ( n + m ) ; compared with AC-4-based trimming, AC-6-based has the same worst-case time of \$\${\textbackslash}mathcal O(n+m)\$\$ O ( n + m ) but an improved worst-case space of \$\${\textbackslash}mathcal O(n)\$\$ O ( n ) . We parallelize the AC-4-based and AC-6-based algorithms to be suitable for shared-memory multi-core machines. The algorithms are designed to minimize synchronization overhead. For these algorithms, we also prove the correctness and analyze time complexities with the work-depth model. In experiments, we compare these three parallel trimming algorithms over a variety of real and synthetic graphs on a multi-core machine, where each core corresponds to a worker. Specifically, for the maximum number of traversed edges per worker by using 16 workers, AC-3-based traverses up to 58.3 and 36.5 times more edges than AC-6-based trimming and AC-4-based trimming, respectively. That is, AC-6-based trimming traverses much fewer edges than other methods, which is meaningful especially for implicit graphs. In particular, for the practical running time, AC-6-based trimming achieves high speedups over graphs with a large portion of trimmable vertices.},
	urldate = {2022-04-18},
	journal = {Journal of Supercomputing},
	author = {Guo, Bin and Sekerinski, Emil},
	month = apr,
	year = {2022},
	pages = {1--45},
}

Given a large data graph, trimming techniques can reduce the search space by removing vertices without outgoing edges. One application is to speed up the parallel decomposition of graphs into strongly connected components (SCC decomposition), which is a fundamental step for analyzing graphs. We observe that graph trimming is essentially a kind of arc-consistency problem, and AC-3, AC-4, and AC-6 are the most relevant arc-consistency algorithms for application to graph trimming. The existing parallel graph trimming methods require worst-case $$\mathcal O(nm)$$ O ( n m ) time and worst-case $$\mathcal O(n)$$ O ( n ) space for graphs with n vertices and m edges. We call these parallel AC-3-based as they are much like the AC-3 algorithm. In this work, we propose AC-4-based and AC-6-based trimming methods. That is, AC-4-based trimming has an improved worst-case time of $$\mathcal O(n+m)$$ O ( n + m ) but requires worst-case space of $$\mathcal O(n+m)$$ O ( n + m ) ; compared with AC-4-based trimming, AC-6-based has the same worst-case time of $$\mathcal O(n+m)$$ O ( n + m ) but an improved worst-case space of $$\mathcal O(n)$$ O ( n ) . We parallelize the AC-4-based and AC-6-based algorithms to be suitable for shared-memory multi-core machines. The algorithms are designed to minimize synchronization overhead. For these algorithms, we also prove the correctness and analyze time complexities with the work-depth model. In experiments, we compare these three parallel trimming algorithms over a variety of real and synthetic graphs on a multi-core machine, where each core corresponds to a worker. Specifically, for the maximum number of traversed edges per worker by using 16 workers, AC-3-based traverses up to 58.3 and 36.5 times more edges than AC-6-based trimming and AC-4-based trimming, respectively. That is, AC-6-based trimming traverses much fewer edges than other methods, which is meaningful especially for implicit graphs. In particular, for the practical running time, AC-6-based trimming achieves high speedups over graphs with a large portion of trimmable vertices.

@misc{GuoEtAl22UniversalDesignPoster,
	address = {Providence, Rhode Island, USA},
	type = {Poster},
	title = {Universal {Design} of {Interactive} {Mathematical} {Notebooks} on {Programming} ({Poster} {Presentation})},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/GuoEtAl22UniversalDesignPoster.webm},
	abstract = {This work presents the rationale behind tools and a guideline for the Universal Design of Jupyter notebooks containing programs, explanations, graphics, algorithms, and proofs, all of which may have mathematical symbols. The tools qualitatively improve accessibility and ease the authoring of such notebooks at the same time. The tools and guidelines are currently being used for a course on concurrent system design and a course on formal languages and compiler construction at McMaster University.},
	author = {Guo, Bin and Nagy, Jason and Sekerinski, Emil},
	month = mar,
	year = {2022},
}

This work presents the rationale behind tools and a guideline for the Universal Design of Jupyter notebooks containing programs, explanations, graphics, algorithms, and proofs, all of which may have mathematical symbols. The tools qualitatively improve accessibility and ease the authoring of such notebooks at the same time. The tools and guidelines are currently being used for a course on concurrent system design and a course on formal languages and compiler construction at McMaster University.

@inproceedings{GuoEtAl22UniversalDesignAbstract,
	title = {Universal {Design} of {Interactive} {Mathematical} {Notebooks} on {Programming} ({Extended} {Abstract})},
	doi = {10.1145/3478432.3499102},
	abstract = {This work presents the rationale behind tools and a guideline for the Universal Design of Jupyter notebooks containing programs, explanations, graphics, algorithms, and proofs, all of which may have mathematical symbols. The tools qualitatively improve accessibility and ease the authoring of such notebooks at the same time. The tools and guidelines are currently being used for a course on concurrent system design and a course on formal languages and compiler construction at McMaster University.},
	booktitle = {Proceedings of the 53rd {ACM} {Technical} {Symposium} on {Computer} {Science} {Education}},
	publisher = {ACM},
	author = {Guo, Bin and Nagy, Jason and Sekerinski, Emil},
	month = mar,
	year = {2022},
	note = {Location: Providence, Rhode Island, USA},
	pages = {1132--1132},
}

This work presents the rationale behind tools and a guideline for the Universal Design of Jupyter notebooks containing programs, explanations, graphics, algorithms, and proofs, all of which may have mathematical symbols. The tools qualitatively improve accessibility and ease the authoring of such notebooks at the same time. The tools and guidelines are currently being used for a course on concurrent system design and a course on formal languages and compiler construction at McMaster University.

@misc{GuoSekerinski22OrderBasedCoreMaintenancePreprint,
	title = {Simplified {Algorithms} for {Order}-{Based} {Core} {Maintenance}},
	doi = {10.48550/arXiv.2201.07103},
	abstract = {Graph analytics attract much attention from both research and
industry communities. Due to the linear time complexity, the 𝑘-
core decomposition is widely used in many real-world applications
such as biology, social networks, community detection, ecology,
and information spreading. In many such applications, the data
graphs continuously change over time. The changes correspond
to edge insertion and removal. Instead of recomputing the 𝑘-core,
which is time-consuming, we study how to maintain the 𝑘-core
efficiently. That is, when inserting or deleting an edge, we need to
identify the affected vertices by searching for more vertices. The
state-of-the-art order-based method maintains an order, the so-
called 𝑘-order, among all vertices, which can significantly reduce
the searching space. However, this order-based method is compli-
cated for understanding and implementation, and its correctness is
not formally discussed. In this work, we propose a simplified order-
based approach by introducing the classical Order Data Structure to
maintain the 𝑘-order, which significantly improves the worst-case
time complexity for both edge insertion and removal algorithms.
Also, our simplified method is intuitive to understand and imple-
ment; it is easy to argue the correctness formally. Additionally,
we discuss a simplified batch insertion approach. The experiments
evaluate our simplified method over 12 real and synthetic graphs
with billions of vertices. Compared with the existing method, our
simplified approach achieves high speedups up to 7.7x and 9.7x for
edge insertion and removal, respectively.},
	publisher = {arXiv},
	author = {Guo, Bin and Sekerinski, Emil},
	month = jan,
	year = {2022},
	note = {Pages: 1-13},
}

Graph analytics attract much attention from both research and industry communities. Due to the linear time complexity, the 𝑘- core decomposition is widely used in many real-world applications such as biology, social networks, community detection, ecology, and information spreading. In many such applications, the data graphs continuously change over time. The changes correspond to edge insertion and removal. Instead of recomputing the 𝑘-core, which is time-consuming, we study how to maintain the 𝑘-core efficiently. That is, when inserting or deleting an edge, we need to identify the affected vertices by searching for more vertices. The state-of-the-art order-based method maintains an order, the so- called 𝑘-order, among all vertices, which can significantly reduce the searching space. However, this order-based method is compli- cated for understanding and implementation, and its correctness is not formally discussed. In this work, we propose a simplified order- based approach by introducing the classical Order Data Structure to maintain the 𝑘-order, which significantly improves the worst-case time complexity for both edge insertion and removal algorithms. Also, our simplified method is intuitive to understand and imple- ment; it is easy to argue the correctness formally. Additionally, we discuss a simplified batch insertion approach. The experiments evaluate our simplified method over 12 real and synthetic graphs with billions of vertices. Compared with the existing method, our simplified approach achieves high speedups up to 7.7x and 9.7x for edge insertion and removal, respectively.

@incollection{MartinHillEtAl22CoCreation,
	title = {Striving {Towards} {Reconciliation} through the {Co}-{Creation} of {Water} {Research}},
	url = {https://doi.org/10.1016/B978-0-12-824538-5.00002-9},
	abstract = {Water issues in Indigenous communities of “Canada” are rooted in the settler-nation’s history of colonialism. Conventional approaches to water management have failed to provide Indigenous communities with water security and limit Indigenous self-determination. Innovative and community-led approaches to water monitoring and management can help promote Indigenous water governance. The Co-Creation of Indigenous Water Quality Tools (CCIWQT) research project is a Haudenosaunee-led approach to improving water security in Six Nations of the Grand River (Six Nations). In alignment with the needs and priorities of Six Nations and underpinned by Haudenosaunee values, the goal of CCIWQT is to develop a broad range of “tools” that can assist in enhancing the community's control over their water management. These tools are being developed through a novel interpretation of co-creation. For CCIWQT, co-creation works to harmonize Indigenous and Western approaches to science by recognizing and respecting the need for knowledge coexistence without assimilation. This Indigenous-led approach to research may be one feasible way to involve non-Indigenous researchers in a reconciliation-based research process that avoids subsuming Indigenous and Local Knowledge into Western ontologies. This book chapter reflects on various reconciliation efforts that were guided by the Indigenous researchers and community members and pursued by the non-Indigenous natural scientists and engineers. Specific CCIWQT research activities are featured to demonstrate how reconciliation “Calls to Action” were applied in practice, while challenges and recommendations are discussed based on the research team's experience.},
	booktitle = {Indigenous {Water} and {Drought} {Management} in a {Changing} {World}},
	publisher = {Elsevier},
	author = {Martin-Hill, Dawn and Gibson, Colin M. and de Lannoy, Charles-François and Gendron, Danielle and McQueen, Denise and Looking Horse, Makasa and King, Clynt and Grewal, Hannah and Deen, Tariq A. and Makhdoom, Sawsan and Chow-Fraser, Patricia and Sekerinski, Emil and Selvaganapathy, P. Ravi and Arain, M. Altaf},
	year = {2022},
	pages = {13--40},
}

Water issues in Indigenous communities of “Canada” are rooted in the settler-nation’s history of colonialism. Conventional approaches to water management have failed to provide Indigenous communities with water security and limit Indigenous self-determination. Innovative and community-led approaches to water monitoring and management can help promote Indigenous water governance. The Co-Creation of Indigenous Water Quality Tools (CCIWQT) research project is a Haudenosaunee-led approach to improving water security in Six Nations of the Grand River (Six Nations). In alignment with the needs and priorities of Six Nations and underpinned by Haudenosaunee values, the goal of CCIWQT is to develop a broad range of “tools” that can assist in enhancing the community's control over their water management. These tools are being developed through a novel interpretation of co-creation. For CCIWQT, co-creation works to harmonize Indigenous and Western approaches to science by recognizing and respecting the need for knowledge coexistence without assimilation. This Indigenous-led approach to research may be one feasible way to involve non-Indigenous researchers in a reconciliation-based research process that avoids subsuming Indigenous and Local Knowledge into Western ontologies. This book chapter reflects on various reconciliation efforts that were guided by the Indigenous researchers and community members and pursued by the non-Indigenous natural scientists and engineers. Specific CCIWQT research activities are featured to demonstrate how reconciliation “Calls to Action” were applied in practice, while challenges and recommendations are discussed based on the research team's experience.

@article{ZhangEtAl21EnsembleLearning,
	title = {Real-time prediction of river chloride concentration using ensemble learning},
	volume = {291},
	doi = {10.1016/j.envpol.2021.118116},
	abstract = {Real-time river chloride prediction has received a lot of attention for its importance in chloride control and management. In this study, an artificial neural network model (i.e., multi-layer perceptron, MLP) and a statistical inference model (i.e., stepwise-cluster analysis, SCA) are developed for predicting chloride concentration in stream water. Then, an ensemble learning model based on MLP and SCA is proposed to further improve the modeling accuracy. A case study of hourly river chloride prediction in the Grand River, Canada is presented to demonstrate the model applicability. The results show that the proposed ensemble learning model, MLP-SCA, provides the best overall performance compared with its two ensemble members in terms of RMSE, MAPE, NSE, and R2 with values of 11.58 mg/L, 27.55\%, 0.90, and 0.90, respectively. Moreover, MLP-SCA is more competent for predicting extremely high chloride concentration. The prediction of observed concentrations above 150 mg/L has RMSE and MAPE values of 9.88 mg/L and 4.40\%, respectively. The outstanding performance of the proposed MLP-SCA, particularly in extreme value prediction, indicates that it can provide reliable chloride prediction using commonly available data (i.e., conductivity, water temperature, river flow rate, and rainfall). The high-frequency prediction of chloride concentration in the Grand River can supplement the existing water quality monitoring programs, and further support the real-time control and management of chloride in the watershed. MLP-SCA is the first ensemble learning model for river chloride prediction and can be extended to other river systems for water quality prediction.},
	journal = {Environmental Pollution},
	author = {Zhang, Qianqian and Li, Zhong and Zhu, Lu and Zhang, Fei and Sekerinski, Emil and Han, Jing-Cheng and Zhou, Yang},
	month = dec,
	year = {2021},
	note = {Publisher: Elsevier},
	pages = {118116},
}

Real-time river chloride prediction has received a lot of attention for its importance in chloride control and management. In this study, an artificial neural network model (i.e., multi-layer perceptron, MLP) and a statistical inference model (i.e., stepwise-cluster analysis, SCA) are developed for predicting chloride concentration in stream water. Then, an ensemble learning model based on MLP and SCA is proposed to further improve the modeling accuracy. A case study of hourly river chloride prediction in the Grand River, Canada is presented to demonstrate the model applicability. The results show that the proposed ensemble learning model, MLP-SCA, provides the best overall performance compared with its two ensemble members in terms of RMSE, MAPE, NSE, and R2 with values of 11.58 mg/L, 27.55%, 0.90, and 0.90, respectively. Moreover, MLP-SCA is more competent for predicting extremely high chloride concentration. The prediction of observed concentrations above 150 mg/L has RMSE and MAPE values of 9.88 mg/L and 4.40%, respectively. The outstanding performance of the proposed MLP-SCA, particularly in extreme value prediction, indicates that it can provide reliable chloride prediction using commonly available data (i.e., conductivity, water temperature, river flow rate, and rainfall). The high-frequency prediction of chloride concentration in the Grand River can supplement the existing water quality monitoring programs, and further support the real-time control and management of chloride in the watershed. MLP-SCA is the first ensemble learning model for river chloride prediction and can be extended to other river systems for water quality prediction.

@misc{GuoNagySekerinski21UniversalDesign,
	address = {Hamilton, Ontario, Canada},
	type = {Poster},
	title = {Universal {Design} of {Interactive} {Notebooks} on {Programming}},
	url = {https://mi.mcmaster.ca/innovations-in-education-conference/},
	abstract = {Jupyter notebooks allow for “interactive textbooks”: programs are embedded in the notebook and can produce textual or graphical output, which is then included in the notebook. Historically they were developed for “reproducible research”, in particular for data analysis, but are now increasingly used for programming courses. This talk presents the rationale behind tools and a guideline for the Universal Design of Jupyter notebooks containing programs, explanations, graphics, algorithms, and proofs, all of which may have mathematical symbols.
The tools improve accessibility for readers and ease the authoring of such notebooks at the same time. The tools and guidelines are currently being used for all material of a course on concurrent system design and a course on formal languages and compiler construction at McMaster. They are open-sourced and can be used for other courses relying on Jupyter notebooks with mathematical, algorithmic, or graphical notation.},
	author = {Guo, Bin and Nagy, Jason and Sekerinski, Emil},
	month = dec,
	year = {2021},
}

Jupyter notebooks allow for “interactive textbooks”: programs are embedded in the notebook and can produce textual or graphical output, which is then included in the notebook. Historically they were developed for “reproducible research”, in particular for data analysis, but are now increasingly used for programming courses. This talk presents the rationale behind tools and a guideline for the Universal Design of Jupyter notebooks containing programs, explanations, graphics, algorithms, and proofs, all of which may have mathematical symbols. The tools improve accessibility for readers and ease the authoring of such notebooks at the same time. The tools and guidelines are currently being used for all material of a course on concurrent system design and a course on formal languages and compiler construction at McMaster. They are open-sourced and can be used for other courses relying on Jupyter notebooks with mathematical, algorithmic, or graphical notation.

@misc{GuoSekerinski21ParallelGraphTrimming,
	type = {Preprint},
	title = {Efficient {Parallel} {Graph} {Trimming} by {Arc}-consistency},
	doi = {10.48550/arXiv.2107.12720},
	abstract = {Given a large data graph, trimming techniques can reduce the search space by removing vertices without outgoing edges. One application is to speed up the parallel decomposition of graphs into strongly connected components (SCC decomposition), which is a fundamental step for analyzing graphs. We observe that graph trimming is essentially a kind of arc-consistency problem, and AC-3, AC-4, and AC-6 are the most relevant arc-consistency algorithms for application to graph trimming. The existing parallel graph trimming methods require worst-case O(nm) time and worst-case O(n) space for graphs with n vertices and m edges. We call these parallel AC-3-based as they are much like the AC-3 algorithm. In this work, we propose AC-4-based and AC-6-based trimming methods. That is, AC-4-based trimming has an improved worst-case time of O(n + m) but requires worst-case space of O(n + m); compared with AC-4-based trimming, AC-6-based has the same worst-case time of O(n + m) but an improved worst-case space of O(n). We parallelize the AC-4-based and AC-6-based algorithms to be suitable for shared-memory multi-core machines. The algorithms are designed to minimize synchronization overhead. For these algorithms, we also prove the correctness and analyze time complexities with the work-depth model.
In experiments, we compare these three parallel trimming algorithms over a variety of real and synthetic graphs. Specifically, for the maximum number of traversed edges per worker by using 16 workers, AC-3-based traverses up to 58.3 and 36.5 times more edges than AC-6-based trimming and AC-4-based trimming, respectively. That is, AC-6-based trimming traverses much fewer edges than other methods, which is meaningful especially for implicit graphs. In particular, for the practical running time, AC-6-based trimming achieves high speedups over graphs with a large portion of trimable vertices.},
	publisher = {arXiv},
	author = {Guo, Bin and Sekerinski, Emil},
	month = jul,
	year = {2021},
	note = {Pages: 1–42},
}

Given a large data graph, trimming techniques can reduce the search space by removing vertices without outgoing edges. One application is to speed up the parallel decomposition of graphs into strongly connected components (SCC decomposition), which is a fundamental step for analyzing graphs. We observe that graph trimming is essentially a kind of arc-consistency problem, and AC-3, AC-4, and AC-6 are the most relevant arc-consistency algorithms for application to graph trimming. The existing parallel graph trimming methods require worst-case O(nm) time and worst-case O(n) space for graphs with n vertices and m edges. We call these parallel AC-3-based as they are much like the AC-3 algorithm. In this work, we propose AC-4-based and AC-6-based trimming methods. That is, AC-4-based trimming has an improved worst-case time of O(n + m) but requires worst-case space of O(n + m); compared with AC-4-based trimming, AC-6-based has the same worst-case time of O(n + m) but an improved worst-case space of O(n). We parallelize the AC-4-based and AC-6-based algorithms to be suitable for shared-memory multi-core machines. The algorithms are designed to minimize synchronization overhead. For these algorithms, we also prove the correctness and analyze time complexities with the work-depth model. In experiments, we compare these three parallel trimming algorithms over a variety of real and synthetic graphs. Specifically, for the maximum number of traversed edges per worker by using 16 workers, AC-3-based traverses up to 58.3 and 36.5 times more edges than AC-6-based trimming and AC-4-based trimming, respectively. That is, AC-6-based trimming traverses much fewer edges than other methods, which is meaningful especially for implicit graphs. In particular, for the practical running time, AC-6-based trimming achieves high speedups over graphs with a large portion of trimable vertices.

@misc{SekerinskiEtAl21ExtendingReMote,
	type = {Poster},
	title = {Extending the re:mote system for water quality measurements and turtle tracking using mobile devices and {Bluetooth}-enabled sensors},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiEtAl21ExtendingReMote.pdf},
	author = {Sekerinski, Emil and Pandya, Dhrumil and Nayeem, Waseef and Srivasanthakumar, Varshan},
	month = may,
	year = {2021},
}

@inproceedings{FadhelSekerinski21Striffs,
	title = {Striffs: {Architectural} component diagrams for code reviews},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/FadhelSekerinski21StriffsPreview.pdf},
	doi = {10.1109/ICCQ51190.2021.9392939},
	abstract = {Despite recent advancements in automated code quality and defect finding tools, developers spend a significant amount of time completing code reviews. Code understandability is a key contributor to this phenomenon, since engineers need to understand both microscopic and macroscopic level details of the code under review. Existing tools for code reviews including diffing, inline commenting and syntax highlighting provide limited support for the macroscopic understanding needs of reviewers. When reviewing code for architectural and design quality, such tools do not enable reviewers to understand the code from a top-down lens which the original architects of the code would have likely used to design the system. To overcome these limitations and to complement existing approaches, we introduce structure diff (striff) diagrams. Striffs provide reviewers with an architectural understanding of the incoming code in relation to the existing system, allowing reviewers to gain a more complete view of the scope and impact of the proposed code changes in a code review.},
	booktitle = {2021 {International} {Conference} on {Code} {Quality} ({ICCQ})},
	publisher = {IEEE},
	author = {Fadhel, Muntazir and Sekerinski, Emil},
	editor = {Zykov, Sergey},
	month = mar,
	year = {2021},
	pages = {69--78},
}

Despite recent advancements in automated code quality and defect finding tools, developers spend a significant amount of time completing code reviews. Code understandability is a key contributor to this phenomenon, since engineers need to understand both microscopic and macroscopic level details of the code under review. Existing tools for code reviews including diffing, inline commenting and syntax highlighting provide limited support for the macroscopic understanding needs of reviewers. When reviewing code for architectural and design quality, such tools do not enable reviewers to understand the code from a top-down lens which the original architects of the code would have likely used to design the system. To overcome these limitations and to complement existing approaches, we introduce structure diff (striff) diagrams. Striffs provide reviewers with an architectural understanding of the incoming code in relation to the existing system, allowing reviewers to gain a more complete view of the scope and impact of the proposed code changes in a code review.

@book{SekerinskiEtAl20FMWS2,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Formal {Methods}. {FM} 2019 {International} {Workshops} - {Porto}, {Portugal}, {October} 7-11, 2019, {Revised} {Selected} {Papers}, {Part} {II}},
	volume = {12233},
	isbn = {978-3-030-54996-1},
	url = {https://doi.org/10.1007/978-3-030-54997-8},
	publisher = {Springer},
	editor = {Sekerinski, Emil and Moreira, Nelma and Oliveira, José N. and Ratiu, Daniel and Guidotti, Riccardo and Farrell, Marie and Luckcuck, Matt and Marmsoler, Diego and Campos, José and Astarte, Troy and Gonnord, Laure and Cerone, Antonio and Couto, Luis and Dongol, Brijesh and Kutrib, Martin and Monteiro, Pedro and Delmas, David},
	year = {2020},
	doi = {10.1007/978-3-030-54997-8},
}

@book{SekerinskiEtAl20FMWS1,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Formal {Methods}. {FM} 2019 {International} {Workshops} - {Porto}, {Portugal}, {October} 7-11, 2019, {Revised} {Selected} {Papers}, {Part} {I}},
	volume = {12232},
	isbn = {978-3-030-54993-0},
	url = {https://doi.org/10.1007/978-3-030-54994-7},
	publisher = {Springer},
	editor = {Sekerinski, Emil and Moreira, Nelma and Oliveira, José N. and Ratiu, Daniel and Guidotti, Riccardo and Farrell, Marie and Luckcuck, Matt and Marmsoler, Diego and Campos, José and Astarte, Troy and Gonnord, Laure and Cerone, Antonio and Couto, Luis and Dongol, Brijesh and Kutrib, Martin and Monteiro, Pedro and Delmas, David},
	year = {2020},
	doi = {10.1007/978-3-030-54994-7},
}

@inproceedings{Sekerinski19DisappearingFormalMethod,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Teaching {Concurrency} with the {Disappearing} {Formal} {Method}},
	volume = {11758},
	isbn = {978-3-030-32441-4},
	doi = {10.1007/978-3-030-32441-4_9},
	abstract = {The Gries-Owicki non-interference condition is fundamental to concurrent programming, but difficult to explain as it relies on proof outlines rather than only pre- and postconditions. This paper reports on teaching a practical course on concurrent programming using hierarchical state diagrams to visualize concurrent programs and argue for their correctness, including non-interference.},
	booktitle = {Formal {Methods} {Teaching}, {Third} {International} {Workshop} and {Tutorial}},
	publisher = {Springer},
	author = {Sekerinski, Emil},
	editor = {Dongol, Brijesh and Petre, Luigia and Smith, Graeme},
	month = oct,
	year = {2019},
	keywords = {Guarded commands, Non-interference, State diagrams},
	pages = {135--149},
}

The Gries-Owicki non-interference condition is fundamental to concurrent programming, but difficult to explain as it relies on proof outlines rather than only pre- and postconditions. This paper reports on teaching a practical course on concurrent programming using hierarchical state diagrams to visualize concurrent programs and argue for their correctness, including non-interference.

@misc{SekerinskiEtAl19ReMotePoster,
	address = {Saskatoon, SK, Canada},
	type = {Poster},
	title = {re:mote – {Low}-cost {Software} and {Hardware} {Infrastructure} for {Water} {Quality} {Sensing} in {Indigenous} {Communities}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiEtAl19ReMotePoster.pdf},
	abstract = {The re:mote software and hardware infrastructure comprises motes with various (commercial and research prototype) sensors for collecting water quality data, a mesh network connecting motes through a base station to a server, a time series database and a (multi-lingual) web server running on the server hardware, and notebooks for analyzing data programmatically. Only open-source software and low-cost hardware are used, allowing the setup to be used for education and maintained by communities. An overview with a demonstration is given.},
	author = {Sekerinski, Emil and Elaghoury, Hassan and Fadhel, Muntazir and Park, Spencer and Singh, Harneet and Tan, Ricardo and Tyrrell, Ryan and Vezina, Victor and Wang, Xi and Yang, Wang and Yao, Shucai},
	month = may,
	year = {2019},
}

The re:mote software and hardware infrastructure comprises motes with various (commercial and research prototype) sensors for collecting water quality data, a mesh network connecting motes through a base station to a server, a time series database and a (multi-lingual) web server running on the server hardware, and notebooks for analyzing data programmatically. Only open-source software and low-cost hardware are used, allowing the setup to be used for education and maintained by communities. An overview with a demonstration is given.

@inproceedings{FadhelSekerinskiYao18TimeSeriesDatabases,
	series = {Advances in {Intelligent} {Systems} and {Computing}},
	title = {A {Comparison} of {Time} {Series} {Databases} for {Storing} {Water} {Quality} {Data}},
	volume = {909},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/FadhelSekerinskiYao18TimeSeriesDatabasesSlides.pdf},
	doi = {10.1007/978-3-030-11434-3_33},
	abstract = {Water quality is an ongoing concern and wireless water qual- ity sensing promises societal benefits. Our goal is to contribute to a low- cost water quality sensing system. The particular focus of this work is the selection of a database for storing water quality data. Recently, time series databases have gained popularity. This paper formulates criteria for comparison, measures selected databases and makes a recommendation for a specific database. A low-cost low-power server, such as a Raspberry Pi, can handle as many as 450 sensors’ data at the same time by using the InfluxDB time series database.},
	booktitle = {Mobile {Technologies} and {Applications} for the {Internet} of {Things}, {IMCL} 2018},
	publisher = {Springer},
	author = {Fadhel, Muntazir and Sekerinski, Emil and Yao, Shucai},
	editor = {Auer, M. and Tsiatsos, T.},
	month = apr,
	year = {2019},
	pages = {302--313},
}

Water quality is an ongoing concern and wireless water qual- ity sensing promises societal benefits. Our goal is to contribute to a low- cost water quality sensing system. The particular focus of this work is the selection of a database for storing water quality data. Recently, time series databases have gained popularity. This paper formulates criteria for comparison, measures selected databases and makes a recommendation for a specific database. A low-cost low-power server, such as a Raspberry Pi, can handle as many as 450 sensors’ data at the same time by using the InfluxDB time series database.

@inproceedings{CoppEtAl19GrabSamples,
	title = {When {Grab} {Samples} {Just} {Won}’t do: {High}-{Quality} {High}-{Frequency} {Water} {Quality} {Monitoring}},
	shorttitle = {{CoppEtAl19GrabSamples}.pdf, {CoppEtAl19GrabSamplesSlides}.pdf},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/CoppEtAl19GrabSamplesSlides.pdf},
	abstract = {The adoption of water quality sensors in wastewater treatment facilities has created a need for protocols to assess the quality of the data. Typically, grab samples analyzed in the laboratory are used for recalibration or sensor matrix adjustments; however, this approach assumes no error in the laboratory-determined value and does not consider the errors in the sampling, sample preparation and laboratory procedures. The goal of this project has been three-fold: what level of error exists in the laboratory values; what level of sensor maintenance is required to improve the measurement accuracy; and, what advantages are gained by the short-term installation of high-frequency sensors. This paper discusses the installation of an RSM30 self-contained monitoring station with two high-frequency ammonia sensors in the primary effluent of the Dundas WWTP. The monitoring provided dynamic loading information for modelling purposes and an opportunity to study the impacts of maintenance on data quality.},
	booktitle = {48th {Annual} {WEAO} {Technical} {Symposium} \& {OPCEA} {Exhibition}},
	publisher = {Water Environment Association of Ontario},
	author = {Copp, John B. and Pooni, Prabhbir and Lai, Winfield and Wang, Xi and Viveros, Roman and Sekerinski, Emil},
	month = apr,
	year = {2019},
	pages = {1--4},
}

The adoption of water quality sensors in wastewater treatment facilities has created a need for protocols to assess the quality of the data. Typically, grab samples analyzed in the laboratory are used for recalibration or sensor matrix adjustments; however, this approach assumes no error in the laboratory-determined value and does not consider the errors in the sampling, sample preparation and laboratory procedures. The goal of this project has been three-fold: what level of error exists in the laboratory values; what level of sensor maintenance is required to improve the measurement accuracy; and, what advantages are gained by the short-term installation of high-frequency sensors. This paper discusses the installation of an RSM30 self-contained monitoring station with two high-frequency ammonia sensors in the primary effluent of the Dundas WWTP. The monitoring provided dynamic loading information for modelling purposes and an opportunity to study the impacts of maintenance on data quality.

@inproceedings{WangSekerinskiCopp19AnomalyDetection,
	title = {Automated {Detection} of {Anomalies} in {High} {Frequency} {Water} {Quality} {Sensor} {Data} using {Machine} {Learning}},
	shorttitle = {{WangSekerinskiCopp19AnomalyDetection}.pdf},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/WangSekerinskiCopp19AnomalyDetection.pdf},
	abstract = {Wastewater treatment facilities are increasingly installing high frequency water quality sensors, which has created a need for automated tools to assess the quality of that data and signal for maintenance as the need arises. As these datasets have increased in size and complexity, it has become difficult to identify problems in a timely manner either manually or using simple rules that might have been sufficient previously. Two high frequency ammonia sensors were installed in November 2017 by Primodal in the primary effluent of the Dundas Wastewater Treatment Plant. Primary effluent ammonia is influenced by daily, seasonal and weather issues and thus exhibits typical stochastic behaviour. The algorithms developed in this project consider periodicity and make use of machine learning techniques to distinguish these issues, with the predicted anomalous data flagged and qualitatively ranked based on the severity and likelihood that the data are faulty.},
	booktitle = {48th {Annual} {WEAO} {Technical} {Symposium} \& {OPCEA} {Exhibition}},
	publisher = {Water Environment Association of Ontario},
	author = {Wang, Xi and Sekerinski, Emil and Copp, John},
	month = apr,
	year = {2019},
	pages = {--116},
}

Wastewater treatment facilities are increasingly installing high frequency water quality sensors, which has created a need for automated tools to assess the quality of that data and signal for maintenance as the need arises. As these datasets have increased in size and complexity, it has become difficult to identify problems in a timely manner either manually or using simple rules that might have been sufficient previously. Two high frequency ammonia sensors were installed in November 2017 by Primodal in the primary effluent of the Dundas Wastewater Treatment Plant. Primary effluent ammonia is influenced by daily, seasonal and weather issues and thus exhibits typical stochastic behaviour. The algorithms developed in this project consider periodicity and make use of machine learning techniques to distinguish these issues, with the predicted anomalous data flagged and qualitatively ranked based on the severity and likelihood that the data are faulty.

@inproceedings{ParkSekerinski18NotebookDesignEmbeddedSystems,
	series = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},
	title = {A {Notebook} {Format} for the {Holistic} {Design} of {Embedded} {Systems} ({Tool} {Paper})},
	volume = {284},
	url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?FIDE2018},
	doi = {10.4204/EPTCS.284.7},
	abstract = {This paper proposes the use of notebooks for the design documentation and tool interaction in the rigorous design of embedded systems. Conventionally, a notebook is a sequence of cells alternating between (textual) code and prose to form a document that is meant to be read from top to bottom, in the spirit of literate programming. We extend the use of notebooks to embedded systems specified by pCharts. The charts are visually edited in cells inline. Other cells can contain statements that generate code and analyze the charts qualitatively and quantitatively; in addition, notebook cells can contain other instructions to build the product from the generated code. This allows a notebook to be replayed to re-analyze the design and re-build the product, like a script, but also allows the notebook to be used for presentations, as for this paper, and for the inspection of the design. The interaction with the notebook is done through a web browser that connects to a local or remote server, thus allowing a computationally intensive analysis to run remotely if needed. The pState notebooks are implemented as an extension to Jupyter. The underlying software architecture is described and the issue of proper placement of transition labels in charts embedded in notebooks is discussed.},
	booktitle = {Proceedings 4th {Workshop} on {Formal} {Integrated} {Development} {Environment}, {Oxford}, {England}, 14 {July} 2018},
	publisher = {Open Publishing Association},
	author = {Park, Spencer and Sekerinski, Emil},
	editor = {Masci, Paolo and Monahan, Rosemary and Prevosto, Virgile},
	month = nov,
	year = {2018},
	pages = {85--94},
}

This paper proposes the use of notebooks for the design documentation and tool interaction in the rigorous design of embedded systems. Conventionally, a notebook is a sequence of cells alternating between (textual) code and prose to form a document that is meant to be read from top to bottom, in the spirit of literate programming. We extend the use of notebooks to embedded systems specified by pCharts. The charts are visually edited in cells inline. Other cells can contain statements that generate code and analyze the charts qualitatively and quantitatively; in addition, notebook cells can contain other instructions to build the product from the generated code. This allows a notebook to be replayed to re-analyze the design and re-build the product, like a script, but also allows the notebook to be used for presentations, as for this paper, and for the inspection of the design. The interaction with the notebook is done through a web browser that connects to a local or remote server, thus allowing a computationally intensive analysis to run remotely if needed. The pState notebooks are implemented as an extension to Jupyter. The underlying software architecture is described and the issue of proper placement of transition labels in charts embedded in notebooks is discussed.

@inproceedings{SekerinskiYao18RefiningSanta,
	series = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},
	title = {Refining {Santa}: {An} {Exercise} in {Efficient} {Synchronization}},
	volume = {282},
	url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?Refine2018},
	doi = {10.4204/EPTCS.282.6},
	abstract = {The Santa Claus Problem is an intricate exercise for concurrent programming. This paper outlines the refinement steps to develop a highly efficient implementation with concurrent objects, starting from a simple specification. The efficiency of the implementation is compared to those in other languages.},
	booktitle = {Proceedings 18th {Refinement} {Workshop}, {Oxford}, {UK}, 18th {July} 2018},
	publisher = {Open Publishing Association},
	author = {Sekerinski, Emil and Yao, Shucai},
	editor = {Derrick, John and Dongol, Brijesh and Reeves, Steve},
	month = oct,
	year = {2018},
	pages = {68--86},
}

The Santa Claus Problem is an intricate exercise for concurrent programming. This paper outlines the refinement steps to develop a highly efficient implementation with concurrent objects, starting from a simple specification. The efficiency of the implementation is compared to those in other languages.

@misc{Sekerinski18MultiCoreEraSlides,
	address = {Hamilton, Ontario, Canada},
	type = {Talk},
	title = {Programming in the {Multi}-{Core} {Era}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski18MultiCoreEraSlides.pdf},
	author = {Sekerinski, Emil},
	month = jun,
	year = {2018},
}

@article{BurtonSekerinski18ObjectModelDynamicMixins,
	title = {An object model for dynamic mixins},
	volume = {51},
	doi = {10.1016/j.cl.2017.07.001},
	abstract = {Dynamic mixins allow objects to be modified at runtime with modular extensions. In applications where method calls must traverse through multiple extensions, a performance penalty relative to static inheritance is realized as receivers of super-calls must be determined at run-time. This work describes an object model which significantly reduces this penalty. The approach is described in terms of a statically typed dynamic mixin-based language called mix.},
	journal = {Computer Languages, Systems \& Structures},
	author = {Burton, Eden and Sekerinski, Emil},
	month = jan,
	year = {2018},
	keywords = {Mixins, Object models, Programming language implementations},
	pages = {90--101},
}

Dynamic mixins allow objects to be modified at runtime with modular extensions. In applications where method calls must traverse through multiple extensions, a performance penalty relative to static inheritance is realized as receivers of super-calls must be determined at run-time. This work describes an object model which significantly reduces this penalty. The approach is described in terms of a statically typed dynamic mixin-based language called mix.

@inproceedings{NokovicSekerinski17ModellingProbabilisticTimingAnalysis,
	title = {Work-in-progress: modelling probabilistic timing analysis},
	doi = {https://doi.org/10.1145/3125503.3125566},
	abstract = {We describe the process of calculating the execution time profile (ETP) in order to determine the probabilistic worst case execution time (WCET) using a model-based approach. By hierarchical state machines with probabilistic transitions and costs/reward specifications, we model the instructions with probabilistic execution time. From the model, our tool, pState, generates input code for a probabilistic model checker on which properties can be analysed.},
	booktitle = {Proceedings of the {Thirteenth} {ACM} {International} {Conference} on {Embedded} {Software} 2017 {Companion}, {EMSOFT} '17},
	publisher = {ACM},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	month = oct,
	year = {2017},
	pages = {4:1--4:2},
}

We describe the process of calculating the execution time profile (ETP) in order to determine the probabilistic worst case execution time (WCET) using a model-based approach. By hierarchical state machines with probabilistic transitions and costs/reward specifications, we model the instructions with probabilistic execution time. From the model, our tool, pState, generates input code for a probabilistic model checker on which properties can be analysed.

@inproceedings{NokovicSekerinski17Tags,
	address = {Grenoble, France},
	title = {Analysis and {Implementation} of {Embedded} {System} {Models}: {Example} of {Tags} in {Item} {Management} {Application}},
	isbn = {978-3-319-47307-9},
	url = {http://dx.doi.org/10.1007/978-3-319-47307-9_7},
	doi = {10.1007/978-3-319-47307-9_7},
	booktitle = {Model-{Implementation} {Fidelity} in {Cyber} {Physical} {System} {Design}},
	publisher = {Springer},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Molnos, Anca and Fabre, Christian},
	year = {2017},
	pages = {175--199},
}

@inproceedings{BurtonSekerinski16ObjectModelMixin,
	address = {Pisa, Italy},
	title = {An {Object} {Model} for a {Dynamic} {Mixin} {Based} {Language}},
	doi = {10.1145/2851613.2851755},
	abstract = {Dynamic mixins allow objects to be modified at runtime with modular extensions. Runtime extensions complicate the object memory management because the order in which mixins are added is not known at compile time. Furthermore, the exact type of the receiver of an up-call from a mixin must be determined at runtime. This work proposes an object model used to address both of these issues. It is used to implement a dynamic mixin-based language called mix and removes the burden of object memory management from the application developer.},
	booktitle = {Proceedings of the 31st {Annual} {ACM} {Symposium} on {Applied} {Computing}, {Object} {Oriented} {Programming} {Languages} and {Systems} {Track}},
	publisher = {ACM},
	author = {Burton, Eden and Sekerinski, Emil},
	month = apr,
	year = {2016},
	keywords = {mixins, object models, programming language implementations},
	pages = {1986--1992},
}

Dynamic mixins allow objects to be modified at runtime with modular extensions. Runtime extensions complicate the object memory management because the order in which mixins are added is not known at compile time. Furthermore, the exact type of the receiver of an up-call from a mixin must be determined at runtime. This work proposes an object model used to address both of these issues. It is used to implement a dynamic mixin-based language called mix and removes the burden of object memory management from the application developer.

@book{PetreSekerinski16ActionToDistributed,
	title = {From {Action} {Systems} to {Distributed} {Systems}—{The} {Refinement} {Approach}},
	url = {https://www.crcpress.com/From-Action-Systems-to-Distributed-Systems-The-Refinement-Approach/Petre-Sekerinski/p/book/9781498701587},
	abstract = {Formal methods traditionally address the question of transforming software engineering into a mature engineering discipline. This essentially refers to trusting that the software-intensive systems that form our society’s infrastructures are behaving according to their specifications. More recently, formal methods are also used to understand properties and evolution laws of existing complex and adaptive systems—man-made such as smart electrical grids or natural ones such as biological networks.

A tribute to Professor Kaisa Sere’s contributions to the field of computer science, From Action Systems to Distributed Systems: The Refinement Approach is the first book to address the impact of refinement through a multitude of formal methods ranging from Action Systems to numerous related approaches in computer science research. It presents a state-of-the-art review on the themes of distributed systems and refinement.

A fundamental part of Kaisa Sere’s research consisted of developing Action Systems, a formalism for modeling, analysing, and constructing distributed systems. Within the design of distributed systems, Kaisa Sere’s main research focus was on refinement-based approaches to the construction of systems ranging from pure software to hardware and digital circuits.

Presenting scientific contributions from renowned researchers around the world, this edited book consists of five sections: Modeling, Analysis, Proof, Refinement, and Applications. Each chapter has been thoroughly reviewed by experts in the field. The book covers both traditional aspects in formal methods research, as well as current and innovative research directions. It describes the transition from the strong theory of refinement to a methodology that can be applied in practice, with tool support.

Examining industrial applications of the methods discussed, this book is a suitable resource for graduate students, researchers, and practitioners interested in using formal methods to develop distributed systems of quality.},
	publisher = {Chapman and Hall/CRC},
	editor = {Petre, Luigia and Sekerinski, Emil},
	month = apr,
	year = {2016},
	doi = {10.1201/b20053},
}

Formal methods traditionally address the question of transforming software engineering into a mature engineering discipline. This essentially refers to trusting that the software-intensive systems that form our society’s infrastructures are behaving according to their specifications. More recently, formal methods are also used to understand properties and evolution laws of existing complex and adaptive systems—man-made such as smart electrical grids or natural ones such as biological networks. A tribute to Professor Kaisa Sere’s contributions to the field of computer science, From Action Systems to Distributed Systems: The Refinement Approach is the first book to address the impact of refinement through a multitude of formal methods ranging from Action Systems to numerous related approaches in computer science research. It presents a state-of-the-art review on the themes of distributed systems and refinement. A fundamental part of Kaisa Sere’s research consisted of developing Action Systems, a formalism for modeling, analysing, and constructing distributed systems. Within the design of distributed systems, Kaisa Sere’s main research focus was on refinement-based approaches to the construction of systems ranging from pure software to hardware and digital circuits. Presenting scientific contributions from renowned researchers around the world, this edited book consists of five sections: Modeling, Analysis, Proof, Refinement, and Applications. Each chapter has been thoroughly reviewed by experts in the field. The book covers both traditional aspects in formal methods research, as well as current and innovative research directions. It describes the transition from the strong theory of refinement to a methodology that can be applied in practice, with tool support. Examining industrial applications of the methods discussed, this book is a suitable resource for graduate students, researchers, and practitioners interested in using formal methods to develop distributed systems of quality.

@inproceedings{NokovicSekerinski16GreatLakes,
	series = {Lecture {Notes} of the {Institute} for {Computer} {Sciences}, {Social} {Informatics} and {Telecommunications} {Engineering}},
	title = {Automatic {Quantitative} {Analysis} and {Code} {Generator} for {Sensor} {Systems}: {The} {Example} of {Great} {Lakes} {Water} {Quality} {Monitoring}},
	volume = {170},
	isbn = {978-3-319-47075-7},
	url = {http://dx.doi.org/10.1007/978-3-319-47075-7_35},
	doi = {10.1007/978-3-319-47075-7_35},
	abstract = {In model-driven development of embedded systems, one would ideally automate both the code generation from the model and the analysis of the model for functional correctness, liveness, timing guarantees, and quantitative properties. Characteristically for embedded systems, analyzing quantitative properties like resource consumption and performance requires a model of the environment as well. We use pState to analyze the power consumption of motes intended for water qual- ity monitoring of recreational beaches in Lake Ontario. We show how system properties can be analyzed by model checking rather than by classical approach based on a functional breakdown and spreadsheet calculation. From the same model, it is possible to generate a framework of executable code to be run on the sensor’s microcontroller. The goal of model checking approach is an improvement of engineering efficiency.},
	booktitle = {Internet of {Things}. {IoT} {Infrastructures}: {Second} {International} {Summit}, {IoT} 360º 2015},
	publisher = {Springer},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Mandler, Benny and Marquez-Barja, Johann and Mitre Campista, Miguel Elias and Cagáňová, Dagmar and Chaouchi, Hakima and Zeadally, Sherali and Badra, Mohamad and Giordano, Stefano and Fazio, Maria and Somov, Andrey and Vieriu, Radu-Laurentiu},
	year = {2016},
	note = {URL: http://s-cubeconference.org/2015/show/program-final},
	pages = {313--319},
}

In model-driven development of embedded systems, one would ideally automate both the code generation from the model and the analysis of the model for functional correctness, liveness, timing guarantees, and quantitative properties. Characteristically for embedded systems, analyzing quantitative properties like resource consumption and performance requires a model of the environment as well. We use pState to analyze the power consumption of motes intended for water qual- ity monitoring of recreational beaches in Lake Ontario. We show how system properties can be analyzed by model checking rather than by classical approach based on a functional breakdown and spreadsheet calculation. From the same model, it is possible to generate a framework of executable code to be run on the sensor’s microcontroller. The goal of model checking approach is an improvement of engineering efficiency.

@inproceedings{NokovicSekerinski15WCETinvariants,
	series = {Electronic {Communications} of the {EASST}},
	title = {Model-based {WCET} {Analysis} with {Invariants}},
	volume = {72},
	doi = {10.14279/tuj.eceasst.72.1026.1010},
	abstract = {The integration of worst-case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations com- pared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs.},
	booktitle = {Proceedings of the 15th {International} {Workshop} on {Automated} {Verification} of {Critical} {Systems}, {AVoCS} 2015},
	publisher = {European Association of Software Science and Technology},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Grov, Gudmund and Ireland, Andrew},
	month = sep,
	year = {2015},
	pages = {1--15},
}

The integration of worst-case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations com- pared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs.

@inproceedings{NokovicSekerinski15HolisticEmbeddedSystem,
	series = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},
	title = {A {Holistic} {Approach} in {Embedded} {System} {Development}},
	volume = {187},
	url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2015.6},
	doi = {10.4204/EPTCS.187.6},
	abstract = {We present pState, a tool for developing “complex” embedded systems by integrating validation into the design process. The goal is to reduce validation time. To this end, qualitative and quantitative properties are specified in system models expressed as pCharts, an extended version of hierarchical state machines. These properties are specified in an intuitive way such that they can be written by engineers who are domain experts, without needing to be familiar with temporal logic. From the system model, executable code that preserves the verified properties is generated. The design is documented on the model and the documentation is passed as comments into the generated code. On the series of examples we illustrate how models and properties are specified using pState.},
	booktitle = {Proceedings {Second} {International} {Workshop} on {Formal} {Integrated} {Development} {Environment}},
	publisher = {Open Publishing Association},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Dubois, Catherine and Masci, Paolo and Méry, Dominique},
	month = jun,
	year = {2015},
	pages = {72--85},
}

We present pState, a tool for developing “complex” embedded systems by integrating validation into the design process. The goal is to reduce validation time. To this end, qualitative and quantitative properties are specified in system models expressed as pCharts, an extended version of hierarchical state machines. These properties are specified in an intuitive way such that they can be written by engineers who are domain experts, without needing to be familiar with temporal logic. From the system model, executable code that preserves the verified properties is generated. The design is documented on the model and the documentation is passed as comments into the generated code. On the series of examples we illustrate how models and properties are specified using pState.

@inproceedings{BurtonSekerinski15MixinSafety,
	title = {The {Safety} of {Dynamic} {Mixin} {Composition}},
	doi = {10.1145/2695664.2695938},
	abstract = {Dynamic mixins are a modular means of developing features or roles that can be composed with objects at run-time. However, naive use of this construct can cause unexpected behaviour due to interference caused by the presence of an object's previously bound mixins. This work proposes a method for developing mixins that can be bound to base ob- jects such that the mixins do not interfere with each other; the method achieves compositionally through a coupling in- variant and by syntactically restricting mixins. The refine- ment calculus is used for formalization, as it treats imple- mentations and specifications uniformly. The formalization relies on a new notion of mixin refinement.},
	booktitle = {Proceedings of the 30th {Annual} {ACM} {Symposium} on {Applied} {Computing}, {SAC}'15, {Object} {Oriented} {Programming} {Languages} and {Systems} {Track}},
	publisher = {ACM},
	author = {Burton, Eden and Sekerinski, Emil},
	month = apr,
	year = {2015},
	pages = {1992--1999},
}

Dynamic mixins are a modular means of developing features or roles that can be composed with objects at run-time. However, naive use of this construct can cause unexpected behaviour due to interference caused by the presence of an object's previously bound mixins. This work proposes a method for developing mixins that can be bound to base ob- jects such that the mixins do not interfere with each other; the method achieves compositionally through a coupling in- variant and by syntactically restricting mixins. The refine- ment calculus is used for formalization, as it treats imple- mentations and specifications uniformly. The formalization relies on a new notion of mixin refinement.

@misc{NokovicSekerinski15TagsPresentation.pdf,
	address = {Grenoble, France},
	type = {Talk},
	title = {Analysis and {Implementation} of {Embedded} {System} {Models}: {Example} of {Tags} in {Item} {Management} {Application}},
	copyright = {https://www.date-conference.com/date15/conference/workshop-w01},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski15TagsPresentation.pdf},
	abstract = {We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. To this end, we use, pState, a tool for the design and verification of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process (MDP) or a Probabilistic Timed Automaton (PTA). On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of tag collection to calculate collision probability and then we use the calculated collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	month = mar,
	year = {2015},
}

We use an application with electronic tags to illustrate a holistic development approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. To this end, we use, pState, a tool for the design and verification of hierarchical state machines extended with probabilistic transitions, costs/rewards, and state invariants, called pCharts. From a pChart, pState generates input code for a probabilistic model checker in the form of either a Markov Decision Process (MDP) or a Probabilistic Timed Automaton (PTA). On the generated model, qualitative and quantitative properties can be verified. From sub-charts without probabilistic transitions, pState can generate executable code in C or assembly language. We analyze the tag collection and collision arbitration of the DASH-7 open standard protocol in which message collision is allowed to some extent. First, we create a model of tag collection to calculate collision probability and then we use the calculated collision probability to estimate the average tag power consumption. Finally, we show how the code for a tag micro-controller can be generated directly from an embedded system model.

@techreport{SekerinskiZhang14PatternsInLime,
	type = {{CAS} {Technical} {Report}},
	title = {Generic {Parallel} {Patterns} in {Lime}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang14PatternsInLime.pdf},
	abstract = {Lime is a heterogeneous computing language currently being developed at IBM Research1 [Auerbach et al., 2010]. It is designed to be executable across a broad range of architectures, including CPUs, GPUs, and FPGAs. The novel features of Lime include limiting side-effects and integration of the streaming paradigm into an object- oriented language. Lime extends Java 1.6 as specified by [Gosling et al., 2005]. A design pattern is a reusable solution for a category of problems [Gamma et al., 1995]. Design patterns offer software developers a repertoire of proven solutions that can be tailored for needs. They are highly popular for object-oriented programming and are being used for concurrent and parallel programming. In this document we present a Lime generic implementation of nine parallel design patterns2. The first seven patterns, namely fork-join, parallel generator, map, recurrence, stencil, reduction and scan, are taken from [McCool et al., 2012] except parallel generator (which is a variation of fork-join). The last two patterns, namely “divide and conquer differently” and “divide and conquer”, the latter one being a special case of the former one, are extracted from various applications. We divide the package into three parts: “common”, which defines patterns and operations that are used by other packages; “testcases”, which includes simple examples that can be used for testing the Lime environment; “examples”, which consists of practical problems that can be solved using the generic patterns.},
	institution = {McMaster University},
	author = {Sekerinski, Emil and Zhang, Tian},
	month = nov,
	year = {2014},
	pages = {24},
}

Lime is a heterogeneous computing language currently being developed at IBM Research1 [Auerbach et al., 2010]. It is designed to be executable across a broad range of architectures, including CPUs, GPUs, and FPGAs. The novel features of Lime include limiting side-effects and integration of the streaming paradigm into an object- oriented language. Lime extends Java 1.6 as specified by [Gosling et al., 2005]. A design pattern is a reusable solution for a category of problems [Gamma et al., 1995]. Design patterns offer software developers a repertoire of proven solutions that can be tailored for needs. They are highly popular for object-oriented programming and are being used for concurrent and parallel programming. In this document we present a Lime generic implementation of nine parallel design patterns2. The first seven patterns, namely fork-join, parallel generator, map, recurrence, stencil, reduction and scan, are taken from [McCool et al., 2012] except parallel generator (which is a variation of fork-join). The last two patterns, namely “divide and conquer differently” and “divide and conquer”, the latter one being a special case of the former one, are extracted from various applications. We divide the package into three parts: “common”, which defines patterns and operations that are used by other packages; “testcases”, which includes simple examples that can be used for testing the Lime environment; “examples”, which consists of practical problems that can be solved using the generic patterns.

@book{AlbertSekerinski14iFM,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Integrated {Formal} {Methods}–11th {International} {Conference}, {IFM} 2014, {Bertinoro}, {Italy}},
	volume = {8739},
	publisher = {Springer},
	editor = {Albert, Elvira and Sekerinski, Emil},
	month = sep,
	year = {2014},
	doi = {10.1007/978-3-319-10181-1},
}

@inproceedings{NokovicSekerinski14TimedpCharts,
	title = {Verification and {Code} {Generation} for {Timed} {Transitions} in {pCharts}},
	doi = {10.1145/2641483.2641522},
	abstract = {This paper describes timed transition in pCharts, a variation of statecharts extended with probabilistic transitions, costs/rewards, and state invariants. Timed transitions with nondeterministic and stochastic timing can be used for the specification and analysis of real-time systems. We present a translation scheme for timed transition of pCharts into probabilistic timed automata (PTA) and executable C code, as implemented in our tool pState. To illustrate the development process, we analyze the power consumption of a radio-frequency identification (RFID) tag and generate code for the PIC micro-controller.},
	booktitle = {{C3S2E} '14: {Proceedings} of the 2014 {International} {C}* {Conference} on {Computer} {Science} \& {Software} {Engineering}},
	publisher = {ACM},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Desai, Bipin C.},
	month = aug,
	year = {2014},
	pages = {3:1--3:10},
}

This paper describes timed transition in pCharts, a variation of statecharts extended with probabilistic transitions, costs/rewards, and state invariants. Timed transitions with nondeterministic and stochastic timing can be used for the specification and analysis of real-time systems. We present a translation scheme for timed transition of pCharts into probabilistic timed automata (PTA) and executable C code, as implemented in our tool pState. To illustrate the development process, we analyze the power consumption of a radio-frequency identification (RFID) tag and generate code for the PIC micro-controller.

@inproceedings{BurtonSekerinski14MixinsDesignPatterns,
	series = {{EuroPLoP} '14},
	title = {Using {Dynamic} {Mixins} to {Implement} {Design} {Patterns}},
	doi = {10.1145/2721956.2721991},
	abstract = {Design patterns are used as a means of documenting solutions to commonly occurring problems. In this work, we focus on object-oriented patterns that require object extension. Typically, the implementation of such patterns is done using object composition. Dynamic mixin composition is proposed as a viable alternative in this paper. The issues of safety and reuse are considered during the comparison of the two approaches. A new mixin language is defined to illustrate the benefits of mixin composition. Then, a survey of sample GOF pattern implementations using both approaches is critiqued and finally some patterns specifically designed to address the shortcomings of object composition are critically reviewed.},
	booktitle = {Proceedings of the 19th {European} {Conference} on {Pattern} {Languages} of {Programs}},
	publisher = {ACM},
	author = {Burton, Eden and Sekerinski, Emil},
	editor = {Heesch, Uwe van},
	month = jul,
	year = {2014},
	pages = {14:1--14:19},
}

Design patterns are used as a means of documenting solutions to commonly occurring problems. In this work, we focus on object-oriented patterns that require object extension. Typically, the implementation of such patterns is done using object composition. Dynamic mixin composition is proposed as a viable alternative in this paper. The issues of safety and reuse are considered during the comparison of the two approaches. A new mixin language is defined to illustrate the benefits of mixin composition. Then, a survey of sample GOF pattern implementations using both approaches is critiqued and finally some patterns specifically designed to address the shortcomings of object composition are critically reviewed.

@misc{NokovicSekerinski14ModellingMotes,
	type = {Poster},
	title = {Modelling {Power} {Consumption} and {Transmission} {Reliability} of {Motes}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski14ModellingMotes.pdf},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	month = jul,
	year = {2014},
}

@techreport{MooreOlivaSekerinskiYao14MultiThreadedStack,
	type = {{CAS} {Technical} {Report}},
	title = {A {Comparison} of {Scalable} {Multi}-{Threaded} {Stack} {Mechanisms}},
	copyright = {http://www.cas.mcmaster.ca/cas/0reports/CAS-14-07-ES.pdf},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/MooreOlivaSekerinskiYao14MultiThreadedStack.pdf},
	abstract = {In the commonly used multi-threaded memory layout where each thread has its ”worst case” stack memory exclusively reserved, a process may prematurely run out of memory, even if there is unused address space elsewhere. This problem is exacerbated as the number of threads in a process increases since there is less stack space available per thread.
In this paper, stack mechanisms that attempt to alleviate this problem are reviewed, and a new stack mechanism is put forward that utilizes the MMU to detect stack overflow. An experimental compiler is used to implement promising stack mechanisms and a suite of benchmarks is used to compare their performance and scalability under varying usage profiles.},
	number = {CAS-14-07-ES},
	institution = {McMaster University},
	author = {Moore-Oliva, Joshua and Sekerinski, Emil and Yao, Shucai},
	month = apr,
	year = {2014},
	pages = {10},
}

In the commonly used multi-threaded memory layout where each thread has its ”worst case” stack memory exclusively reserved, a process may prematurely run out of memory, even if there is unused address space elsewhere. This problem is exacerbated as the number of threads in a process increases since there is less stack space available per thread. In this paper, stack mechanisms that attempt to alleviate this problem are reviewed, and a new stack mechanism is put forward that utilizes the MMU to detect stack overflow. An experimental compiler is used to implement promising stack mechanisms and a suite of benchmarks is used to compare their performance and scalability under varying usage profiles.

@techreport{SekerinskiZhang14CaseStudiesHeterogenerousParallelism,
	type = {{CAS} {Technical} {Report}},
	title = {Case {Studies} in {Program} {Design} for {Heterogeneous} {Parallelism}},
	copyright = {http://www.cas.mcmaster.ca/cas/0reports/CAS-14-03-ES.pdf},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang14CaseStudiesHeterogenerousParallelism.pdf},
	abstract = {This collection is the outcome of students projects of the graduate course CAS 766 Concurrent Programming at McMaster University in the fall of 2013. The projects are on heteroge- neous computing, the execution of program on a combination of CPUs, FPGAs and GPUs. With processor frequencies having reached a ceiling (for a number of years already!) and power consumption limiting the complexity of single (multi-core) CPUs, heterogeneous computing has the promise of speeding up computations through parallelism while reducing power consumption. The last point is essential for everything from mobile devices to server farms. However, heterogeneous computing requires a different programming model than the traditional models of shared variables and message passing.},
	number = {CAS-14-03-ES},
	institution = {McMaster University},
	author = {Sekerinski, Emil and Zhang, Tian},
	month = mar,
	year = {2014},
	pages = {171},
}

This collection is the outcome of students projects of the graduate course CAS 766 Concurrent Programming at McMaster University in the fall of 2013. The projects are on heteroge- neous computing, the execution of program on a combination of CPUs, FPGAs and GPUs. With processor frequencies having reached a ceiling (for a number of years already!) and power consumption limiting the complexity of single (multi-core) CPUs, heterogeneous computing has the promise of speeding up computations through parallelism while reducing power consumption. The last point is essential for everything from mobile devices to server farms. However, heterogeneous computing requires a different programming model than the traditional models of shared variables and message passing.

@inproceedings{SekerinskiZhang13FinitaryFairness,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Finitary {Fairness} in {Action} {Systems}},
	volume = {8049},
	isbn = {978-3-642-39717-2},
	url = {http://dx.doi.org/10.1007/978-3-642-39718-9_19},
	doi = {10.1007/978-3-642-39718-9_19},
	abstract = {In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.},
	booktitle = {Theoretical {Aspects} of {Computing}–{ICTAC} 2013, 10th {International} {Colloquium}},
	publisher = {Springer},
	author = {Sekerinski, Emil and Zhang, Tian},
	editor = {Liu, Zhiming and Woodcock, Jim and Zhu, Huibiao},
	month = sep,
	year = {2013},
	keywords = {Event-B, Finitary Fairness, Modelling, Stepwise Refinement, Termination},
	pages = {319--336},
}

In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.

@inproceedings{NokovicSekerinski13pState,
	title = {{pState}: {A} {Probabilistic} {Statecharts} {Translator}},
	doi = {10.1109/MECO.2013.6601339},
	abstract = {We describe pState, an experimental so ware toolkit for the design, validation and formal veri cation of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems. Costs/rewards can be used to compute quantitative properties such as expected power consumption or expected number of lost messages in model of some communication protocol. State invariants are used to express safety conditions or consistency constraints. The charts are validated and transformed into an intermediate representation, from which code for various languages can be generated.},
	booktitle = {Embedded {Computing} ({MECO}), 2nd {Mediterranean} {Conference} on},
	publisher = {IEEE Press},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	editor = {Stojanović, Radovan and Jóźwiak, Lech and Lutovac, Budimir},
	month = jun,
	year = {2013},
	keywords = {Computational modeling, invariants, model-checking, quantitative properties, statecharts, verification},
	pages = {29--32},
}

We describe pState, an experimental so ware toolkit for the design, validation and formal veri cation of complex systems. Classical statecharts are extended with probabilistic transitions, costs/rewards, and state invariants. Probabilistic choice can be used to model randomized algorithms or unreliable systems. Costs/rewards can be used to compute quantitative properties such as expected power consumption or expected number of lost messages in model of some communication protocol. State invariants are used to express safety conditions or consistency constraints. The charts are validated and transformed into an intermediate representation, from which code for various languages can be generated.

@inproceedings{BurtonSekerinski13CorrectnessIntrusiveDataStructures,
	series = {{CBSE} '13},
	title = {Correctness of intrusive data structures using mixins},
	isbn = {978-1-4503-2122-8},
	url = {http://doi.acm.org/10.1145/2465449.2465466},
	doi = {10.1145/2465449.2465466},
	abstract = {A dynamic mixin is a code fragment that is meant to be dynamically bound to an object. Dynamic mixins support more flexible code composition than class inheritance and can be used to implement roles that objects acquire dynamically. We propose a theory, based on data refinement, for reasoning about the correctness of programs with mixins. The theory is suited for applications of mixins to intrusive data structures, where the data structure is spread over existing objects. We illustrate this with two examples, one-to-one association and union-find data structures.},
	booktitle = {Proceedings of the 16th {International} {ACM} {Sigsoft} {Symposium} on {Component}-{Based} {Software} {Engineering}},
	publisher = {ACM},
	author = {Burton, Eden and Sekerinski, Emil},
	month = jun,
	year = {2013},
	keywords = {mixins, refinements},
	pages = {53--58},
}

A dynamic mixin is a code fragment that is meant to be dynamically bound to an object. Dynamic mixins support more flexible code composition than class inheritance and can be used to implement roles that objects acquire dynamically. We propose a theory, based on data refinement, for reasoning about the correctness of programs with mixins. The theory is suited for applications of mixins to intrusive data structures, where the data structure is spread over existing objects. We illustrate this with two examples, one-to-one association and union-find data structures.

@inproceedings{SekerinskiZhang13PartialRefinement,
	series = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},
	title = {On a {New} {Notion} of {Partial} {Refinement}},
	volume = {115},
	url = {http://arxiv.org/abs/1305.6110v1},
	doi = {10.4204/EPTCS.115.1},
	abstract = {Formal specification techniques allow expressing idealized specifications, which abstract from re- strictions that may arise in implementations. However, partial implementations are universal in soft- ware development due to practical limitations. Our goal is to contribute to a method of program refinement that allows for partial implementations. For programs with a normal and an exceptional exit, we propose a new notion of partial refinement which allows an implementation to terminate ex- ceptionally if the desired results cannot be achieved, provided the initial state is maintained. Partial refinement leads to a systematic method of developing programs with exception handling.},
	booktitle = {Proceedings of the 16th {International} {Refinement} {Workshop}},
	publisher = {Open Publishing Association},
	author = {Sekerinski, Emil and Zhang, Tian},
	editor = {Derrick, John and Boiten, Eerke and Reeves, Steve},
	month = may,
	year = {2013},
	pages = {1 -- 14},
}

Formal specification techniques allow expressing idealized specifications, which abstract from re- strictions that may arise in implementations. However, partial implementations are universal in soft- ware development due to practical limitations. Our goal is to contribute to a method of program refinement that allows for partial implementations. For programs with a normal and an exceptional exit, we propose a new notion of partial refinement which allows an implementation to terminate ex- ceptionally if the desired results cannot be achieved, provided the initial state is maintained. Partial refinement leads to a systematic method of developing programs with exception handling.

@inproceedings{SekerinskiZhang12ExceptionHandlingEiffel,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Verification {Rules} for {Exception} {Handling} in {Eiffel}},
	volume = {7498},
	isbn = {978-3-642-33295-1},
	doi = {10.1007/978-3-642-33296-8_14},
	abstract = {The Eiffel exception mechanism supports two methodological aspects. First, a method specification by a pre- and postcondition also determines when the method exits exceptionally, namely when the stated postcondition cannot be satisfied. Secondly, the rescue and retry statements combine catching an exception with a loop structure, thus requiring a dedicated form of correctness reasoning. We present verification rules for total correctness that take these two aspects into account. The rules handle normal loops and retry loop structures in an analogous manner. They also allow the Eiffel's mechanism to be slightly generalized. The verification rules are derived from a definition of statements by higher-order predicate transformers and have been checked with a theorem prover.},
	booktitle = {Formal {Methods}: {Foundations} and {Applications}},
	publisher = {Springer},
	author = {Sekerinski, Emil and Zhang, Tian},
	editor = {Gheyi, Rohit and Naumann, David},
	month = sep,
	year = {2012},
	pages = {179--193},
}

The Eiffel exception mechanism supports two methodological aspects. First, a method specification by a pre- and postcondition also determines when the method exits exceptionally, namely when the stated postcondition cannot be satisfied. Secondly, the rescue and retry statements combine catching an exception with a loop structure, thus requiring a dedicated form of correctness reasoning. We present verification rules for total correctness that take these two aspects into account. The rules handle normal loops and retry loop structures in an analogous manner. They also allow the Eiffel's mechanism to be slightly generalized. The verification rules are derived from a definition of statements by higher-order predicate transformers and have been checked with a theorem prover.

@misc{Sekerinski12TutorialExceptionHandling,
	address = {Abo Akademi, Turku, Finland},
	type = {Tutorial},
	title = {Tutorial on {Exception} {Handling}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski12TutorialExceptionHandling.pdf},
	author = {Sekerinski, Emil},
	month = feb,
	year = {2012},
}

@incollection{Sekerinski11ExceptionsDependability,
	title = {Exceptions for {Dependability}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski11ExceptionsDependability.pdf},
	abstract = {Exception handling allows a program to be structured such that the original design can be preserved in presence of possibly failing components, it allows for an unobtrusive treatment of rare or undesired cases, and can be used to address imperfections in programs. This chapter develops a theory of exception handling with try-catch statements and shows its use in the design of dependable systems by giving a formal account of the patterns of masking, propagating, flagging, rollback, degraded service, recovery block, repeated attempts, and conditional retry. The theory is based on weakest exceptional preconditions, which are used for both defining statements and for proofs. Proof outlines are introduced and used to establish the correctness of the patterns.},
	booktitle = {Dependability and {Computer} {Engineering}: {Concepts} for {Software}-{Intensive} {Systems}—a {Handbook} on {Dependability} {Research}},
	publisher = {IGI Global},
	author = {Sekerinski, Emil},
	editor = {Petre, Luigia and Sere, Kaisa and Troubitsyna, Elena},
	month = jul,
	year = {2011},
	doi = {10.4018/978-1-60960-747-0},
	pages = {11--35},
}

Exception handling allows a program to be structured such that the original design can be preserved in presence of possibly failing components, it allows for an unobtrusive treatment of rare or undesired cases, and can be used to address imperfections in programs. This chapter develops a theory of exception handling with try-catch statements and shows its use in the design of dependable systems by giving a formal account of the patterns of masking, propagating, flagging, rollback, degraded service, recovery block, repeated attempts, and conditional retry. The theory is based on weakest exceptional preconditions, which are used for both defining statements and for proofs. Proof outlines are introduced and used to establish the correctness of the patterns.

@inproceedings{SekerinskiZhang11PartialCorrectness,
	title = {A {New} {Notion} of {Partial} {Correctness} for {Exception} {Handling}},
	copyright = {https://ece.uwaterloo.ca/ bbonakda/LAFT11/papers/proc.pdf},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/BonakdarpourMaibaum11LAFT.pdf},
	abstract = {We study the correctness of programs that use exception handling to deal with failures. A new notion of partial correctness is introduced for the design of programs that can continue safely after an unanticipated failure. Partial correctness is contrasted with total correctness though their verification rules. These rules are derived from a definition of statements with exceptions as higher order predicate transformers. The use of total and partial correctness is illustrated with three design patterns, rollback, degraded service, and recovery block.},
	booktitle = {Proceedings of the 2nd {International} {Workshop} on {Logical} {Aspects} of {Fault}-{Tolerance}},
	author = {Sekerinski, Emil and Zhang, Tian},
	editor = {Bonakdarpour, Borzoo and Maibaum, Tom},
	month = jun,
	year = {2011},
	pages = {116--132},
}

We study the correctness of programs that use exception handling to deal with failures. A new notion of partial correctness is introduced for the design of programs that can continue safely after an unanticipated failure. Partial correctness is contrasted with total correctness though their verification rules. These rules are derived from a definition of statements with exceptions as higher order predicate transformers. The use of total and partial correctness is illustrated with three design patterns, rollback, degraded service, and recovery block.

@techreport{NokovicSekerinski11PowerModelling,
	type = {{SQRL} {Report}},
	title = {Power {Modelling} and {Power} {Analysis} of {Electronic} {Tag}: {A} {Case} {Study} {Using} {Probabilistic} {Model} {Checking}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski11PowerModelling.pdf},
	abstract = {In this work we study methods for computing the daily power consumption of an electronic tag, a battery-powered mobile device used in postal systems. First, we calculate the power consumption with “paper and pencil” by building FSM model of a device and identified all activities as possible sources of power consumption. In next step, we show how the number of activities can be reduced by combining them. Then a model is designed as a discrete-time Markov chain with rewards. Quantitative properties are specified in probabilistic linear temporal logic and automatically analyzed by the probabilistic model checker PRISM. With our model, we verify that the sleep mode accounts for the biggest share of total power consumption and that a possible decrease of power consumption during communication will not lead to a significant decrease in overall power consumption. While this calculation is done for a simple tag that is currently in use, the goal is to apply this method to more complex tags currently under development.},
	number = {63},
	institution = {McMaster University},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	month = apr,
	year = {2011},
	pages = {14},
}

In this work we study methods for computing the daily power consumption of an electronic tag, a battery-powered mobile device used in postal systems. First, we calculate the power consumption with “paper and pencil” by building FSM model of a device and identified all activities as possible sources of power consumption. In next step, we show how the number of activities can be reduced by combining them. Then a model is designed as a discrete-time Markov chain with rewards. Quantitative properties are specified in probabilistic linear temporal logic and automatically analyzed by the probabilistic model checker PRISM. With our model, we verify that the sleep mode accounts for the biggest share of total power consumption and that a possible decrease of power consumption during communication will not lead to a significant decrease in overall power consumption. While this calculation is done for a simple tag that is currently in use, the goal is to apply this method to more complex tags currently under development.

@techreport{SekerinskiZingaro11Pascal0,
	type = {{CAS} {Technical} {Report}},
	title = {Pascal0 {Compiler}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZingaro11Pascal0.pdf},
	abstract = {Pascal0 is a subset of the Pascal programming language, suited for teaching the principles of compiler construction. This report describes a one-pass recursive descent compiler for Pascal0. The compiler is written in Pascal and generates code for RISC, a register-based instruction set, and STACK, a stack-oriented instruction set. Interpreters for RISC and STACK are included; these allow the execution of the generated code to be traced. The presentation of the compiler exemplifies modularization and documentation principles. This document is written using the noweb literate programming tool. The Pascal source code is automatically extracted from this document.},
	institution = {McMaster University},
	author = {Sekerinski, Emil and Zingaro, Daniel},
	month = jan,
	year = {2011},
	pages = {48},
}

Pascal0 is a subset of the Pascal programming language, suited for teaching the principles of compiler construction. This report describes a one-pass recursive descent compiler for Pascal0. The compiler is written in Pascal and generates code for RISC, a register-based instruction set, and STACK, a stack-oriented instruction set. Interpreters for RISC and STACK are included; these allow the execution of the generated code to be traced. The presentation of the compiler exemplifies modularization and documentation principles. This document is written using the noweb literate programming tool. The Pascal source code is automatically extracted from this document.

@techreport{SekerinskiZhang11NormalFormMultiExit,
	type = {{CAS} {Technical} {Report}},
	title = {A {Normal} {Form} for {Multi}-{Exit} {Statements}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang11NormalFormMultiExit.pdf},
	abstract = {For a class of statements, a normal form provides a uniform way for their formal specification. Control structures like exception handling introduce additional exit(s) of statements, and new normal forms as a consequence. In this paper, we give the normal forms of several classes of multi-exit statements, explore their algebraic properties, and discuss their potential of being utilized for the development of programs, where a postcondition for each exit is required. All the theorems have been checked with a formal verification tool.},
	institution = {McMaster University},
	author = {Sekerinski, Emil and Zhang, Tian},
	year = {2011},
	pages = {16},
}

For a class of statements, a normal form provides a uniform way for their formal specification. Control structures like exception handling introduce additional exit(s) of statements, and new normal forms as a consequence. In this paper, we give the normal forms of several classes of multi-exit statements, explore their algebraic properties, and discuss their potential of being utilized for the development of programs, where a postcondition for each exit is required. All the theorems have been checked with a formal verification tool.

@techreport{NokovicSekerinski10Interrogator,
	address = {Hamilton, Ontario, Canada},
	type = {{SQRL} {Report}},
	title = {Analysis of {Interrogator}-tag {Communication} {Protocols}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski10Interrogator.pdf},
	abstract = {In this document we discuss and analyze three different Interrogator-Tag communication protocols. The first protocol is used in the AMQM (Automatic Mail Quality Measurement) system. The second protocol is based on the ISO 18000-7 standard, which specifies the protocol and parameters for active RFID (Radio Frequency IDentification) air interface communication at the 433MHz ISM (Industrial Scientific Medical) band. The third protocol is the AMQM protocol with some features of the ISO 18000-7 standard. Quantitative properties of the protocols are analyzed. The main goal of modelling is to analyze tag message collision probability and power consumption. The model is verified by PRISM - Probabilistic Model Check Software. We showed that by implementing principles of model checking, we could verify probability of reaching a particular state, calculate collision probability as quantitative property, and cost of reaching determined state. We also showed that model of the protocol could be used to estimate possible improvement in a one protocol by implementing features from another protocol.},
	number = {60},
	institution = {McMaster University},
	author = {Nokovic, Bojan and Sekerinski, Emil},
	month = dec,
	year = {2010},
	note = {Pages: 22},
	pages = {20},
}

In this document we discuss and analyze three different Interrogator-Tag communication protocols. The first protocol is used in the AMQM (Automatic Mail Quality Measurement) system. The second protocol is based on the ISO 18000-7 standard, which specifies the protocol and parameters for active RFID (Radio Frequency IDentification) air interface communication at the 433MHz ISM (Industrial Scientific Medical) band. The third protocol is the AMQM protocol with some features of the ISO 18000-7 standard. Quantitative properties of the protocols are analyzed. The main goal of modelling is to analyze tag message collision probability and power consumption. The model is verified by PRISM - Probabilistic Model Check Software. We showed that by implementing principles of model checking, we could verify probability of reaching a particular state, calculate collision probability as quantitative property, and cost of reaching determined state. We also showed that model of the protocol could be used to estimate possible improvement in a one protocol by implementing features from another protocol.

@inproceedings{SekerinskiZhang10FinitaryFairness,
	title = {Finitary {Fairness} in {Event}-{B} ({Extended} {Abstract})},
	copyright = {http://drops.dagstuhl.de/portals/09381/},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang10FinitaryFairness.pdf},
	doi = {10.4230/DagSemProc.09381.1},
	booktitle = {Dagstuhl {Seminar} on {Refinement} {Based} {Methods} for the {Construction} of {Dependable} {Systems}},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
	author = {Sekerinski, Emil and Zhang, Tian},
	editor = {Abrial, Jean-Raymond and Butler, Michael and Joshi, Rajeev and Troubitsyna, Elena and Woodcock, Jim C. P.},
	month = jan,
	year = {2010},
	pages = {1-- 5},
}

@book{MousaviSekerinski09FMDS,
	title = {Proceedings of {Formal} {Methods} 2009 {Doctoral} {Symposium}},
	url = {http://www.win.tue.nl/fm2009/DoctoralSymposium/fm09ds.pdf},
	publisher = {TU Eindhoven},
	editor = {Mousavi, MohammadReza and Sekerinski, Emil},
	month = nov,
	year = {2009},
}

@incollection{Sekerinski09StateInvariants,
	title = {Design {Verification} with {State} {Invariants}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski09StateInvariants.pdf},
	abstract = {This chapter contains sections titled: Introduction Preliminaries Statechart Structure Configurations and Operations State Invariant Verification Accumulated Invariants Verification Condition Generation Priority Among Transitions Conclusions References},
	booktitle = {{UML} 2 {Semantics} and {Applications}},
	publisher = {John Wiley \& Sons},
	author = {Sekerinski, Emil},
	editor = {Lano, Kevin},
	month = oct,
	year = {2009},
	doi = {10.1002/9780470522622.ch13},
	note = {URL: https://onlinelibrary.wiley.com/doi/10.1002/9780470522622.ch13},
	keywords = {accumulated invariants and targeted verification condition generation, design verification with state invariants, self-transition and interlevel transition},
	pages = {317--347},
}

This chapter contains sections titled: Introduction Preliminaries Statechart Structure Configurations and Operations State Invariant Verification Accumulated Invariants Verification Condition Generation Priority Among Transitions Conclusions References

@techreport{CuiSekerinski09ABC,
	address = {Hamilton, Ontario, Canada},
	type = {{SQRL} {Report}},
	title = {An {Experimental} {Implementation} of {Action}-{Based} {Concurrency}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/CuiSekerinski09ABC.pdf},
	abstract = {This paper reports on an experimental implementation of action-based concurrent objects. Concurrency is expressed by allowing objects to have actions with a guard and a body, in addition to methods and variables. Condition synchronization is expressed by method guards protecting entry into an object. An action of an object can execute any time when its guard is true, with the restriction that at most one action or methods can execute within an object, thus guaranteeing atomicity. In principle, all objects can execute in parallel. The appeal of this model is that it is conceptually simple for programmers and comes with a verification and refinement theory based on atomic actions that is a straightforward extension of that for sequential programs. The concurrency model is suited for tightly coupled shared-memory processors. The implementation makes use of a recent thread library, NPTL, that supports a large number of kernel threads. Each active object has its own thread that cycles through the actions, evaluates their guards, and executes an enabled action. Syntactic constraints restrict when guards need to be re-evaluated. We compare the efficiency of the generated code with that of C/Pthreads, Ada, and Java using classical concurrency examples.},
	number = {58},
	institution = {McMaster University},
	author = {Cui, Xiao-lei and Sekerinski, Emil},
	month = jul,
	year = {2009},
	pages = {25},
}

This paper reports on an experimental implementation of action-based concurrent objects. Concurrency is expressed by allowing objects to have actions with a guard and a body, in addition to methods and variables. Condition synchronization is expressed by method guards protecting entry into an object. An action of an object can execute any time when its guard is true, with the restriction that at most one action or methods can execute within an object, thus guaranteeing atomicity. In principle, all objects can execute in parallel. The appeal of this model is that it is conceptually simple for programmers and comes with a verification and refinement theory based on atomic actions that is a straightforward extension of that for sequential programs. The concurrency model is suited for tightly coupled shared-memory processors. The implementation makes use of a recent thread library, NPTL, that supports a large number of kernel threads. Each active object has its own thread that cycles through the actions, evaluates their guards, and executes an enabled action. Syntactic constraints restrict when guards need to be re-evaluated. We compare the efficiency of the generated code with that of C/Pthreads, Ada, and Java using classical concurrency examples.

@inproceedings{Sekerinski09UnifyingMathematicsSoftwareDesign,
	address = {Burnaby, British Columbia, Canada},
	series = {{WCCCE} '09},
	title = {Teaching the {Unifying} {Mathematics} of {Software} {Design}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski09UnifyingMathematicsSoftwareDesignPreprint.pdf},
	doi = {10.1145/1536274.1536307},
	abstract = {We report on our experience on teaching the mathematics of reliable software design as a unifying force for various elements of software design, rather than as an additional element of software design. This is in line with the use of mathematics in traditional engineering disciplines, but in contrast to teaching a “formal method” optionally after an “informal” exposition to software design or teaching a formal method only with specific applications in mind.},
	booktitle = {Proceedings of the 14th {Western} {Canadian} {Conference} on {Computing} {Education}},
	publisher = {ACM},
	author = {Sekerinski, Emil},
	editor = {Brouwer, R. and Cukierman, D. and Tsiknis, G.},
	month = may,
	year = {2009},
	pages = {109--115},
}

We report on our experience on teaching the mathematics of reliable software design as a unifying force for various elements of software design, rather than as an additional element of software design. This is in line with the use of mathematics in traditional engineering disciplines, but in contrast to teaching a “formal method” optionally after an “informal” exposition to software design or teaching a formal method only with specific applications in mind.

@inproceedings{Sekerinski08AlgebraicFairChoice,
	series = {Electronic {Notes} in {Theoretical} {Computer} {Science}},
	title = {An {Algebraic} {Approach} to {Refinement} with {Fair} {Choice}},
	volume = {214},
	doi = {http://dx.doi.org/10.1016/j.entcs.2008.06.004},
	abstract = {In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.},
	booktitle = {Proceedings of the 13th {BAC}-{FACS} {Refinement} {Workshop} ({REFINE} 2008)},
	publisher = {Elsevier},
	author = {Sekerinski, Emil},
	editor = {Boiten, E. and Derrick, J. and Schellhorn, G.},
	month = jun,
	year = {2008},
	keywords = {action systems, alternating bit protocol, fairness, refinement},
	pages = {51--79},
}

In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.

@inproceedings{Sekerinski08StateInvariants,
	address = {Belfast, Northern Ireland},
	series = {{ICECCS} '08},
	title = {Verifying {Statecharts} with {State} {Invariants}},
	doi = {http://dx.doi.org/10.1109/ICECCS.2008.40},
	abstract = {Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating “many small” verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.},
	booktitle = {13th {IEEE} {International} {Conference} on {Engineering} of {Complex} {Computer} {Systems}},
	publisher = {IEEE Computer Society},
	author = {Sekerinski, Emil},
	editor = {Breitman, K. and Woodcock, J. and Sterritt, R. and Hinchey, M.},
	month = mar,
	year = {2008},
	pages = {7--14},
}

Statecharts are an executable visual language for specifying the reactive behavior of systems. We propose to statically verify the design expressed by a statechart by allowing individual states to be annotated with invariants and checking the consistency of the invariants with the transitions. We present an algorithm that uses the locality of state invariants for generating “many small” verification conditions that should be more amenable to automatic checking than an approach based on a single global invariant.

@techreport{Sekerinski07TeachingSoftwareDesign,
	type = {{SQRL} {Report}},
	title = {Teaching the {Unifying} {Mathematics} of {Software} {Design}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski07TeachingSoftwareDesign.pdf},
	abstract = {We report on our experience on teaching the mathematics of software design as a unifying force for various elements of software design, rather than as an additional element of software design. This is in line with the use of mathematics in traditional engineering disciplines, but in contrast to teaching a “formal method” optionally after an “informal” exposition to software design or teaching a formal method only with specific applications in mind.},
	number = {49},
	institution = {McMaster University},
	author = {Sekerinski, Emil},
	month = dec,
	year = {2007},
	pages = {17},
}

We report on our experience on teaching the mathematics of software design as a unifying force for various elements of software design, rather than as an additional element of software design. This is in line with the use of mathematics in traditional engineering disciplines, but in contrast to teaching a “formal method” optionally after an “informal” exposition to software design or teaching a formal method only with specific applications in mind.

@inproceedings{LeSekerinskiWest06StatechartVerification,
	address = {Hamilton, Ontario, Canada},
	title = {Statechart {Verification} with {iState}},
	url = {http://fm06.mcmaster.ca/istate.pdf},
	booktitle = {{FM} 2006: {Formal} {Methods}–{Posters} and {Research} {Tools}},
	publisher = {McMaster University},
	author = {Le, Dai Tri Man and Sekerinski, Emil and West, Scott},
	editor = {Chechik, Marsha},
	month = aug,
	year = {2006},
	pages = {1--6},
}

@inproceedings{Sekerinski06TeachingSoftwareDesign,
	title = {Teaching the {Mathematics} of {Software} {Design}},
	url = {http://www4.di.uminho.pt/FME-SoE/FMEd06/},
	abstract = {This note summarizes the experience and philosophy of teaching two one-semester courses, Software Design 1, a second year course, and Software Design 2, a third year course, repeatedly in the period from 1999/2000 to 2005/06. These courses had a peak enrollment of 190 students. Many students perceive these two courses as the core courses for their career in software development. The same material was presented in a condensed form in a graduate course in 2005/06. The courses taught students the mathematics of software design, rather than a particular “formal method” tool or language.},
	booktitle = {Formal {Methods} in the {Teaching} {Lab}, {Workshop} at the {FM} 2006: {Formal} {Methods} {Symposium}},
	publisher = {University of Minho},
	author = {Sekerinski, Emil},
	editor = {Boute, R. T. and Oliveira, J. N.},
	month = aug,
	year = {2006},
	pages = {53--58},
}

This note summarizes the experience and philosophy of teaching two one-semester courses, Software Design 1, a second year course, and Software Design 2, a third year course, repeatedly in the period from 1999/2000 to 2005/06. These courses had a peak enrollment of 190 students. Many students perceive these two courses as the core courses for their career in software development. The same material was presented in a condensed form in a graduate course in 2005/06. The courses taught students the mathematics of software design, rather than a particular “formal method” tool or language.

@book{MisraNipkowSekerinski06FormalMethods,
	address = {Hamilton, Ontario, Canada},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {{FM} 2006: {Formal} {Methods}–14th {International} {Symposium} on {Formal} {Methods}},
	volume = {4085},
	publisher = {Springer},
	editor = {Misra, Jayadev and Nipkow, Tobias and Sekerinski, Emil},
	month = aug,
	year = {2006},
	doi = {10.1007/11813040},
}

@book{Sekerinski06SoftwareDesign2,
	series = {{SQRL} {Report}},
	title = {Topics in {Software} {Design}. {Volume} 2},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski06SoftwareDesign2.pdf},
	abstract = {This collection of papers is produced by participants of the graduate course CAS 703 Software Design, winter term 2005/06, at McMaster University. The course was divided into two parts. In the first part the instructor gave seminars on fundamental topics in software design. For the record, these were: 1. Elements of Programming 2. Modularization 3. Abstract Programs 4. Testing 5. Exceptions 6. Functional Specifications 7. Object-Oriented Programs 8. Object-Oriented Modelling 9. Requirements Analysis 10. Object-Oriented Design 11. Reactive Programs 12. Configuration Management 13. Software Development Process For the second part, students selected a topic for which they reviewed the literature, gave a presentation, and wrote a paper. This report consists of those papers, in order of presentation. Some of the articles are surveys and some develop new ideas; they are all beyond the material found in textbooks on software design. The topics range from issues in programming languages to programming tools, design principles, pedagogical issues, and managerial issues. All papers are sound starting points for further research.},
	number = {35},
	publisher = {McMaster University},
	editor = {Sekerinski, Emil},
	month = jun,
	year = {2006},
}

This collection of papers is produced by participants of the graduate course CAS 703 Software Design, winter term 2005/06, at McMaster University. The course was divided into two parts. In the first part the instructor gave seminars on fundamental topics in software design. For the record, these were: 1. Elements of Programming 2. Modularization 3. Abstract Programs 4. Testing 5. Exceptions 6. Functional Specifications 7. Object-Oriented Programs 8. Object-Oriented Modelling 9. Requirements Analysis 10. Object-Oriented Design 11. Reactive Programs 12. Configuration Management 13. Software Development Process For the second part, students selected a topic for which they reviewed the literature, gave a presentation, and wrote a paper. This report consists of those papers, in order of presentation. Some of the articles are surveys and some develop new ideas; they are all beyond the material found in textbooks on software design. The topics range from issues in programming languages to programming tools, design principles, pedagogical issues, and managerial issues. All papers are sound starting points for further research.

@book{Sekerinski05SoftwareDesign1,
	series = {{SQRL} {Report}},
	title = {Topics in {Software} {Design}. {Volume} 1},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski05SoftwareDesign1.pdf},
	abstract = {This collection of papers is produced by participants of the graduate course CAS 703 Software Design, winter term 2004/05. The course was divided into two parts. In the first, participants and the instructor gave seminars on fundamental topics in software design. For the second part, students selected a more advanced topic for which they reviewed the literature, gave a presentation, and wrote a paper. This report consists of those papers, in order of presentation. The topics are all on “emerging” issues in software design. Some of the articles are surveys and some develop new ideas; they are all beyond the material found in textbooks on software design. The diversity of themes and the dedication of the authors makes this collection an enjoyable read and insightful read! The collection is recommended to anyone who likes to deepen their understanding of, or engage in research in the respective topic.},
	number = {34},
	publisher = {McMaster University},
	editor = {Sekerinski, Emil},
	month = jun,
	year = {2005},
}

This collection of papers is produced by participants of the graduate course CAS 703 Software Design, winter term 2004/05. The course was divided into two parts. In the first, participants and the instructor gave seminars on fundamental topics in software design. For the second part, students selected a more advanced topic for which they reviewed the literature, gave a presentation, and wrote a paper. This report consists of those papers, in order of presentation. The topics are all on “emerging” issues in software design. Some of the articles are surveys and some develop new ideas; they are all beyond the material found in textbooks on software design. The diversity of themes and the dedication of the authors makes this collection an enjoyable read and insightful read! The collection is recommended to anyone who likes to deepen their understanding of, or engage in research in the respective topic.

@article{Sekerinski05ConcurrentObjects,
	title = {Verification and {Refinement} with {Fine}-{Grained} {Action}-{Based} {Concurrent} {Objects}},
	volume = {331},
	doi = {10.1016/j.tcs.2004.09.024},
	abstract = {Action-based concurrent object-oriented programs express autonomous behavior of objects through actions that, like methods, are attached to objects but, in contrast to methods, may execute autonomously whenever their guard is true. The promise is a streamlining of the program structure by eliminating the distinction between processes and objects and a streamlining of correctness arguments. In this paper we illustrate the use of action-based object-oriented programs and study their verification and their refinement from specifications, including the issue of non-atomic operations.},
	number = {2–3},
	journal = {Theoretical Computer Science},
	author = {Sekerinski, Emil},
	month = feb,
	year = {2005},
	pages = {429--455},
}

Action-based concurrent object-oriented programs express autonomous behavior of objects through actions that, like methods, are attached to objects but, in contrast to methods, may execute autonomously whenever their guard is true. The promise is a streamlining of the program structure by eliminating the distinction between processes and objects and a streamlining of correctness arguments. In this paper we illustrate the use of action-based object-oriented programs and study their verification and their refinement from specifications, including the issue of non-atomic operations.

@inproceedings{LiangSekerinski04IntegratingSpecificationDocumentation,
	address = {Newport Beach, California, USA},
	series = {Workshop of {SIGSOFT} 2004/{FSE}-12, 12th {ACM} {SIGSOFT} {Symposium} on the {Foundations} of {Software} {Engineering}},
	title = {Integrating {Specification} and {Documentation} in an {Object}-oriented {Language}},
	url = {https://www.cs.ucf.edu/~leavens/SAVCBS/2004/savcbs04.pdf},
	abstract = {This paper reports on the integration of specification and documentation features into an object-oriented programming language and its compiler. The goal of this integration is to improve software quality, in particular correctness, extensibility, and maintainability in a uniform and coherent manner. The language taken is Lime, an action-based concurrent object-oriented language developed at McMaster University. The concurrency aspect of Lime is motivated by the observation that concurrency is increasingly used to improve responsiveness of programs. Concurrency in Lime is expressed by attaching actions to objects. This eliminates the conceptual distinction between objects and threads. For the theory behind this approach and an implementation scheme the reader is referred to [12].},
	booktitle = {{SAVCBS} 2004, {Specification} and {Verification} of {Component}-{Based} {Systems}},
	publisher = {Technical Report \#04-09, Department of Computer Science, Iowa State University},
	author = {Liang, Jie and Sekerinski, Emil},
	month = nov,
	year = {2004},
	pages = {126--129},
}

This paper reports on the integration of specification and documentation features into an object-oriented programming language and its compiler. The goal of this integration is to improve software quality, in particular correctness, extensibility, and maintainability in a uniform and coherent manner. The language taken is Lime, an action-based concurrent object-oriented language developed at McMaster University. The concurrency aspect of Lime is motivated by the observation that concurrency is increasingly used to improve responsiveness of programs. Concurrency in Lime is expressed by attaching actions to objects. This eliminates the conceptual distinction between objects and threads. For the theory behind this approach and an implementation scheme the reader is referred to [12].

@article{Sekerinski03TabularVerificationRefinement,
	title = {Exploring {Tabular} {Verification} and {Refinement}},
	volume = {15},
	doi = {10.1007/s00165-003-0010-9},
	abstract = {Tabular representations have been proposed for structuring complex mathematical expressions as they appear in the specification of programs. We argue that tables not only help in writing and checking complex expressions, but also in their formal manipulation. More specifically, we explore the use of tabular predicates and tabular relations in program verification and refinement.},
	number = {2},
	journal = {Formal Aspects of Computing},
	author = {Sekerinski, Emil},
	month = nov,
	year = {2003},
	pages = {215--236},
}

Tabular representations have been proposed for structuring complex mathematical expressions as they appear in the specification of programs. We argue that tables not only help in writing and checking complex expressions, but also in their formal manipulation. More specifically, we explore the use of tabular predicates and tabular relations in program verification and refinement.

@inproceedings{Sekerinski03SimpleCOOP,
	address = {Sveti Stefan, Montenegro},
	title = {A {Simple} {Model} for {Concurrent} {Object}-{Oriented} {Programming}},
	copyright = {http://vipsi.org/ipsi/conferences/},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski03SimpleCOOP.pdf},
	abstract = {It has been argued that objects can be naturally thought of as evolving independently and thus concurrently; an object is a natural ”unit” of concurrency. Yet, current mainstream object-oriented languages treat concurrency independently of objects: concurrency is expressed in terms of threads that have to be managed separately from objects. We argue for a model for concurrent object-oriented programs in which no such distinction is made. The only syntactic additions needed are extending classes by actions and allowing methods to be guarded. Execution is governed by a simple rule for atomicity. The model allows concurrency to be seamlessly introduced in classes, thus for example allowing concurrency to be introduced in subclasses of a class hierarchy. This permits concurrency to be treated as an implementation issue in the same way as the choice of an algorithm. The model relieves the programmer from having to distinguish between the process and class aspects in software design. We illustrate the model by examples, discuss its rationale, and outline our current implementation.},
	booktitle = {International {Conference} {Internet}, {Processing}, {Systems}, {Interdisciplinaries}, {IPSI} 2003},
	author = {Sekerinski, Emil},
	editor = {Milutinovic, Veljko},
	month = oct,
	year = {2003},
	pages = {1--4},
}

It has been argued that objects can be naturally thought of as evolving independently and thus concurrently; an object is a natural ”unit” of concurrency. Yet, current mainstream object-oriented languages treat concurrency independently of objects: concurrency is expressed in terms of threads that have to be managed separately from objects. We argue for a model for concurrent object-oriented programs in which no such distinction is made. The only syntactic additions needed are extending classes by actions and allowing methods to be guarded. Execution is governed by a simple rule for atomicity. The model allows concurrency to be seamlessly introduced in classes, thus for example allowing concurrency to be introduced in subclasses of a class hierarchy. This permits concurrency to be treated as an implementation issue in the same way as the choice of an algorithm. The model relieves the programmer from having to distinguish between the process and class aspects in software design. We illustrate the model by examples, discuss its rationale, and outline our current implementation.

@inproceedings{Sekerinski03COOP,
	address = {Leiden, The Netherlands},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Concurrent {Object}-{Oriented} {Programs}: {From} {Specification} to {Code}},
	volume = {2852},
	doi = {10.1007/978-3-540-39656-7_17},
	abstract = {In this paper we put forward a concurrent object-oriented programming language in which concurrency is tightly integrated with objects. Concurrency is expressed by extending classes with actions and allowing methods to be guarded. Concurrency in an object may be hidden to the outside, thus allowing concurrency to be introduced in subclasses of a class hierarchy. A disciplined form of intra-object concurrency is supported. The language is formally defined by translation to action systems. Inheritance and subtyping is also considered. A theory of class refinement is presented, allowing concurrent programs to be developed from sequential specifications. Our goal is to have direct rules for verification and refinement on one hand and a practical implementation on the other hand. We briefly sketch our implementation. While the implementation relies on threads, the management of threads is hidden to the programmer.},
	booktitle = {Formal {Methods} for {Components} and {Objects}, {First} {International} {Symposium}, {FMCO} 02},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Boer, F. S. de and Bonsangue, M. and Graf, S. and Roever, W.-P. de},
	month = jul,
	year = {2003},
	pages = {403--423},
}

In this paper we put forward a concurrent object-oriented programming language in which concurrency is tightly integrated with objects. Concurrency is expressed by extending classes with actions and allowing methods to be guarded. Concurrency in an object may be hidden to the outside, thus allowing concurrency to be introduced in subclasses of a class hierarchy. A disciplined form of intra-object concurrency is supported. The language is formally defined by translation to action systems. Inheritance and subtyping is also considered. A theory of class refinement is presented, allowing concurrent programs to be developed from sequential specifications. Our goal is to have direct rules for verification and refinement on one hand and a practical implementation on the other hand. We briefly sketch our implementation. While the implementation relies on threads, the management of threads is hidden to the programmer.

@inproceedings{Sekerinski02TabularVerificationRefinement,
	series = {Electronic {Notes} in {Theoretical} {Computer} {Science}},
	title = {Tabular {Verification} and {Refinement}},
	volume = {70},
	doi = {10.1016/S1571-0661(05)80492-X},
	abstract = {Tabular representations have been proposed for structuring mathematical expressions as they appear in the specification of programs. The thesis of this work is that tables not only help in writing and checking complex expressions, but also in their formal manipulation. We consider tabular predicates and tabular relations and their use in program verification and refinement.},
	booktitle = {{REFINE} 2002, {The} {BCS} {FACS} {Refinement} {Workshop}},
	publisher = {Elsevier},
	author = {Sekerinski, Emil},
	editor = {Derrick, John and Boiten, Eerke and Woodcock, Jim and Wright, Joakim von},
	month = jul,
	year = {2002},
	pages = {179--198},
}

Tabular representations have been proposed for structuring mathematical expressions as they appear in the specification of programs. The thesis of this work is that tables not only help in writing and checking complex expressions, but also in their formal manipulation. We consider tabular predicates and tabular relations and their use in program verification and refinement.

@inproceedings{SekerinskiZurob02StatechartsToB,
	address = {Turku, Finland},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Translating {Statecharts} to {B}},
	volume = {2335},
	doi = {10.1007/3-540-47884-1_8},
	abstract = {We present algorithms for the translation of statecharts to the Abstract Machine Notation of the B method. These algorithms have been implemented in {\textbackslash}em iState, a tool for translating statecharts to various programming languages. The translation proceeds in several phases. We give a model of statecharts, a model of the code in AMN, as well as the intermediate representations in terms of class diagrams and their textual counterpart. The translation algorithms are expressed in terms of these models. We also discuss optimizations of the generated code. The translation scheme is motivated by making the generated code comprehensible.},
	booktitle = {Third {International} {Conference} on {Integrated} {Formal} {Methods}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil and Zurob, Rafik},
	editor = {Butler, Michael and Petre, Luigia and Sere, Kaisa},
	month = may,
	year = {2002},
	pages = {128--144},
}

We present algorithms for the translation of statecharts to the Abstract Machine Notation of the B method. These algorithms have been implemented in \em iState, a tool for translating statecharts to various programming languages. The translation proceeds in several phases. We give a model of statecharts, a model of the code in AMN, as well as the intermediate representations in terms of class diagrams and their textual counterpart. The translation algorithms are expressed in terms of these models. We also discuss optimizations of the generated code. The translation scheme is motivated by making the generated code comprehensible.

@inproceedings{SekerinskiZurob01iState,
	address = {Toronto, Canada},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {{iState}: {A} {Statechart} {Translator}},
	volume = {2185},
	doi = {10.1007/3-540-45441-1_28},
	abstract = {We describe formal steps in the design of iState, a tool for translating statecharts into programming languages. Currently iState generates code in either Pascal, Java, or the Abstract Machine Notation of the B method. The translation proceeds in several phases. The focus of this paper is the formal description of the intermediate representations, for which we use class diagrams together with their textual counterparts. We describe how the class diagrams are further refined. The notions of representable, normalized, and legal statecharts are introduced, where normalized statecharts appear as an intermediate representation and code is generated only for legal statecharts.},
	booktitle = {«{UML}» 2001 – {The} {Unified} {Modeling} {Language}, 4th {International} {Conference}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil and Zurob, Rafik},
	editor = {Gogolla, Martin and Kobryn, Cris},
	month = oct,
	year = {2001},
	pages = {376--390},
}

We describe formal steps in the design of iState, a tool for translating statecharts into programming languages. Currently iState generates code in either Pascal, Java, or the Abstract Machine Notation of the B method. The translation proceeds in several phases. The focus of this paper is the formal description of the intermediate representations, for which we use class diagrams together with their textual counterparts. We describe how the class diagrams are further refined. The notions of representable, normalized, and legal statecharts are introduced, where normalized statecharts appear as an intermediate representation and code is generated only for legal statecharts.

@article{JanickiSekerinski01TraceAssertion,
	title = {Foundations of the {Trace} {Assertion} {Method} of {Module} {Interface} {Specification}},
	volume = {27},
	issn = {0098-5589},
	doi = {10.1109/32.935852},
	abstract = {The trace assertion method is a formal state machine based method for specifying module interfaces. A module interface specification treats the module as a black-box, identifying all the module's access programs (i.e., programs that can be invoked from outside of the module) and describing their externally visible effects. In the method, both the module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of nondeterminism, normal and exceptional behavior, value functions, and multiobject modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted.},
	number = {7},
	journal = {IEEE Transactions on Software Engineering},
	author = {Janicki, Ryszard and Sekerinski, Emil},
	month = jul,
	year = {2001},
	keywords = {Mealy machines, Module interface specifications, module refinement, nondeterminism, relational model, state machines, step-sequences, tabular notation., trace assertion method},
	pages = {577--598},
}

The trace assertion method is a formal state machine based method for specifying module interfaces. A module interface specification treats the module as a black-box, identifying all the module's access programs (i.e., programs that can be invoked from outside of the module) and describing their externally visible effects. In the method, both the module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of nondeterminism, normal and exceptional behavior, value functions, and multiobject modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted.

@techreport{SekerinskiZurob01StatechartsToCode,
	type = {{CAS} {Technical} {Report}},
	title = {From {Statecharts} to {Code}: {A} {Tool} for the {Graphical} {Design} of {Reactive} {Systems}},
	institution = {McMaster University},
	author = {Sekerinski, Emil and Zurob, Rafik},
	year = {2001},
}

@article{BuchiSekerinski00RefiningConcurrentObjects,
	title = {A {Foundation} for {Refining} {Concurrent} {Objects}},
	volume = {44},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/BuchiSekerinski00RefiningConcurrentObjectsPreprint.pdf},
	abstract = {We study the notion of class refinement in a concurrent object-oriented setting. Our model is based on a combination of action systems and classes. An action system describes the behavior of a concurrent, distributed, or interactive system in terms of the atomic actions that can take place during the execution of the system. Classes serve as templates for creating objects. To express concurrency with objects, we add actions to classes. We define class refinement based on trace refinement of action systems. Additionally, we give a simulation-based proof rule. We show that the easier to apply simulation rule implies the trace-based definition of class refinement. Class refinement embraces algorithmic refinement, data refinement, and atomicity refinement. Atomicity refinement allows us to split large atomic actions into several smaller ones. Thereby, it paves the way for more parallelism. We investigate the special case of atomicity refinement by early returns in methods.},
	number = {1,2},
	journal = {Fundamenta Informaticae},
	author = {Büchi, Martin and Sekerinski, Emil},
	month = sep,
	year = {2000},
	pages = {25--61},
}

We study the notion of class refinement in a concurrent object-oriented setting. Our model is based on a combination of action systems and classes. An action system describes the behavior of a concurrent, distributed, or interactive system in terms of the atomic actions that can take place during the execution of the system. Classes serve as templates for creating objects. To express concurrency with objects, we add actions to classes. We define class refinement based on trace refinement of action systems. Additionally, we give a simulation-based proof rule. We show that the easier to apply simulation rule implies the trace-based definition of class refinement. Class refinement embraces algorithmic refinement, data refinement, and atomicity refinement. Atomicity refinement allows us to split large atomic actions into several smaller ones. Thereby, it paves the way for more parallelism. We investigate the special case of atomicity refinement by early returns in methods.

@inproceedings{sekerinski_guarded_2000,
	address = {Ponte de Lima, Portugal},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {On {Guarded} {Commands} with {Fair} {Choice}},
	volume = {1837},
	doi = {10.1007/10722010_9},
	abstract = {For the purpose of program development, fairness is typically formalized by verification rules or, alternatively, through refinement rules. In this paper we give an account of (weak) fairness in an algebraic style, extending recently proposed algebraic accounts of iterations and loops using the predicate transformer model of statements.},
	booktitle = {5th {International} {Conference} on the {Mathematics} of {Program} {Construction}, {MPC} 2000},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Backhouse, Roland and Oliveira, Jose},
	month = jul,
	year = {2000},
	note = {CitationKey: Sekerinski00FairChoice},
	pages = {127--139},
}

For the purpose of program development, fairness is typically formalized by verification rules or, alternatively, through refinement rules. In this paper we give an account of (weak) fairness in an algebraic style, extending recently proposed algebraic accounts of iterations and loops using the predicate transformer model of statements.

@inproceedings{MikhajlovSekerinskiLaibinis99ComponentsReentrance,
	address = {Toulouse, France},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Developing {Components} in {Presence} of {Re}-entrance},
	volume = {1709},
	doi = {10.1007/3-540-48118-4_19},
	abstract = {Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.},
	booktitle = {{FM}'99 — {Formal} {Methods}},
	publisher = {Springer-Verlag},
	author = {Mikhajlov, Leonid and Sekerinski, Emil and Laibinis, Linas},
	editor = {Wing, Jeanette and Woodcock, Jim and Davis, Jim},
	month = sep,
	year = {1999},
	pages = {721--721},
}

Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.

@techreport{BuchiSekerinski99RefiningConcurrentObjects,
	type = {{TUCS} {Technical} {Report}},
	title = {Refining {Concurrent} {Objects}},
	url = {http://tucs.fi/publications/view/?pub_id=tBuSe99a},
	abstract = {We study the notion of class refinement in a concurrent object-oriented setting. Classes, defining attributes and methods, serve as templates for creating objects. For expressing concurrency, actions are added to classes and methods with guards are considered. A class can be defined by inheriting from a given class. Class refinement is defined to support algorithmic refinement, data refinement, and atomicity refinement. Behavioral class refinement is defined in terms of trace refinement of action systems. A simulation-based proof rule for class refinement using a refinement relation is given. The special case of atomicity refinement by early returns is considered. The use of the class refinement rule is illustrated by examples.},
	number = {298},
	institution = {Turku Centre for Computer Science},
	author = {Büchi, Martin and Sekerinski, Emil},
	month = aug,
	year = {1999},
	keywords = {ISBN 952-12-0509-1 ISSN 1239-1891},
	pages = {28},
}

We study the notion of class refinement in a concurrent object-oriented setting. Classes, defining attributes and methods, serve as templates for creating objects. For expressing concurrency, actions are added to classes and methods with guards are considered. A class can be defined by inheriting from a given class. Class refinement is defined to support algorithmic refinement, data refinement, and atomicity refinement. Behavioral class refinement is defined in terms of trace refinement of action systems. A simulation-based proof rule for class refinement using a refinement relation is given. The special case of atomicity refinement by early returns is considered. The use of the class refinement rule is illustrated by examples.

@techreport{JanickiSekerinski99TraceAssertion,
	type = {{SERG} {Report}},
	title = {Foundations of the {Trace} {Assertion} {Method} of {Module} {Interface} {Specification}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/JanickiSekerinski99TraceAssertion.pdf},
	abstract = {The trace assertion method is a formal state machine based method for specifying module interfaces. A module interface specification treats the module as a black-box, identifying all module's access programs (i.e. programs that can be invoked from outside of the module), and describing their externally visible effects. In the method, both the module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of non-determinism, normal and exceptional behavior, value functions and multi-object modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted.},
	number = {376},
	institution = {McMaster University},
	author = {Janicki, Ryszard and Sekerinski, Emil},
	month = jul,
	year = {1999},
	pages = {41},
}

The trace assertion method is a formal state machine based method for specifying module interfaces. A module interface specification treats the module as a black-box, identifying all module's access programs (i.e. programs that can be invoked from outside of the module), and describing their externally visible effects. In the method, both the module states and the behaviors observed are fully described by traces built from access program invocations and their visible effects. A formal model for the trace assertion method is proposed. The concept of step-traces is introduced and applied. The stepwise refinement of trace assertion specifications is considered. The role of non-determinism, normal and exceptional behavior, value functions and multi-object modules are discussed. The relationship with algebraic specifications is analyzed. A tabular notation for writing trace specifications to ensure readability is adapted.

@techreport{MikhajlovaSekerinski99CorrectnessJavaFrameworks,
	type = {{TUCS} {Technical} {Report}},
	title = {Ensuring {Correctness} of {Java} {Frameworks}: {A} {Formal} {Look} at {JCF}},
	url = {http://tucs.fi/publications/view/?pub_id=tMiSe99a},
	abstract = {In this paper we propose a novel approach to specification, development, and verification of object-oriented frameworks employing separate interface inheritance and implementation inheritance hierarchies. In particular, we illustrate how our method of framework specification and verification can be used to specify Java Collections Framework, which is a part of the standard Java Development Kit 2.0, and ensure its correctness. We propose to associate with Java interfaces formal descriptions of the behavior that classes implementing these interfaces and their subinterfaces must deliver. Verifying behavioral conformance of classes implementing given interfaces to the specifications integrated with these interfaces allows us to ensure correctness of the system. The characteristic feature of our specification methodology is that the specification language used combines standard executable statements of the Java language with possibly nondeterministic specification statements. A specification of the intended behavior of a particular interface given in this language can serve as a precise documentation guiding implementation development. Since subtyping polymorphism in Java is based on interface inheritance, behavioral conformance of subinterfaces to their superinterfaces is essential for correctness of object substitutability in clients. As we view interfaces augmented with formal specifications as abstract classes, verifying behavioral conformance amounts to proving class refinement between specifications of superinterfaces and subinterfaces. Moreover, the logic framework that we use also allows verification of behavioral conformance between specifications of interfaces and classes implementing these interfaces. The uniform treatment of specifications and implementations and the relationships between them permits verifying correctness of the whole framework and its extensions.},
	number = {250},
	institution = {Turku Centre for Computer Science},
	author = {Mikhajlova, Anna and Sekerinski, Emil},
	month = mar,
	year = {1999},
	pages = {40},
}

In this paper we propose a novel approach to specification, development, and verification of object-oriented frameworks employing separate interface inheritance and implementation inheritance hierarchies. In particular, we illustrate how our method of framework specification and verification can be used to specify Java Collections Framework, which is a part of the standard Java Development Kit 2.0, and ensure its correctness. We propose to associate with Java interfaces formal descriptions of the behavior that classes implementing these interfaces and their subinterfaces must deliver. Verifying behavioral conformance of classes implementing given interfaces to the specifications integrated with these interfaces allows us to ensure correctness of the system. The characteristic feature of our specification methodology is that the specification language used combines standard executable statements of the Java language with possibly nondeterministic specification statements. A specification of the intended behavior of a particular interface given in this language can serve as a precise documentation guiding implementation development. Since subtyping polymorphism in Java is based on interface inheritance, behavioral conformance of subinterfaces to their superinterfaces is essential for correctness of object substitutability in clients. As we view interfaces augmented with formal specifications as abstract classes, verifying behavioral conformance amounts to proving class refinement between specifications of superinterfaces and subinterfaces. Moreover, the logic framework that we use also allows verification of behavioral conformance between specifications of interfaces and classes implementing these interfaces. The uniform treatment of specifications and implementations and the relationships between them permits verifying correctness of the whole framework and its extensions.

@techreport{MikhajlovSekerinskiLaibinis99ComponentsReentranceReport,
	type = {{TUCS} {Technical} {Report}},
	title = {Developing {Components} in {Presence} of {Re}-entrance},
	url = {http://tucs.fi/publications/view/?pub_id=tMiSeLa99a},
	abstract = {Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.},
	number = {239},
	institution = {Turku Centre for Computer Science},
	author = {Mikhajlov, Leonid and Sekerinski, Emil and Laibinis, Linas},
	month = feb,
	year = {1999},
	keywords = {ISBN 952-12-0382-X ISSN 1239-1891},
	pages = {25},
}

Independent development of components according to their specifications is complicated by the fact that a thread of control can exit and re-enter the same component. This kind of re-entrance may cause problems as the internal representation of a component can be observed in an inconsistent state. We argue that the ad-hoc reasoning used in establishing conformance of components to their specifications that intuitively appears to be correct does not account for the presence of re-entrance. Such reasoning leads to a conflict between assumptions that component developers make about the behavior of components in a system, resulting in the component re-entrance problem. We formulate the modular reasoning property that captures the process of independent component development and introduce two requirements that must be imposed to avoid the re-entrance problem. Then we define a customized theory of components, component systems, and component refinement which models the process of component development from specifications. Using this theory, we prove that the formulated requirements are sufficient to establish the modular reasoning property.

@inproceedings{MikhajlovSekerinski98FragileBaseClassProblem,
	address = {Brussels, Belgium},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {A {Study} of the {Fragile} {Base} {Class} {Problem}},
	volume = {1445},
	doi = {10.1007/BFb0054099},
	abstract = {In this paper we study the fragile base class problem. This problem occurs in open object-oriented systems employing code inheritance as an implementation reuse mechanism. System developers unaware of extensions to the system developed by its users may produce a seemingly acceptable revision of a base class which may damage its extensions. The fragile base class problem becomes apparent during maintenance of open object-oriented systems, but requires consideration during design. We express the fragile base class problem in terms of a flexibility property. By means of five orthogonal examples, violating the flexibility property, we demonstrate different aspects of the problem. We formulate requirements for disciplining inheritance, and extend the refinement calculus to accommodate for classes, objects, class-based inheritance, and class refinement. We formulate and formally prove a flexibility theorem demonstrating that the restrictions we impose on inheritance are sufficient to permit safe substitution of a base class with its revision in presence of extension classes.},
	booktitle = {{ECOOP}'98 — 12th {European} {Conference} on {Object}-{Oriented} {Programming}},
	publisher = {Springer-Verlag},
	author = {Mikhajlov, Leonid and Sekerinski, Emil},
	editor = {Jul, Eric},
	month = jul,
	year = {1998},
	pages = {355--382},
}

In this paper we study the fragile base class problem. This problem occurs in open object-oriented systems employing code inheritance as an implementation reuse mechanism. System developers unaware of extensions to the system developed by its users may produce a seemingly acceptable revision of a base class which may damage its extensions. The fragile base class problem becomes apparent during maintenance of open object-oriented systems, but requires consideration during design. We express the fragile base class problem in terms of a flexibility property. By means of five orthogonal examples, violating the flexibility property, we demonstrate different aspects of the problem. We formulate requirements for disciplining inheritance, and extend the refinement calculus to accommodate for classes, objects, class-based inheritance, and class refinement. We formulate and formally prove a flexibility theorem demonstrating that the restrictions we impose on inheritance are sufficient to permit safe substitution of a base class with its revision in presence of extension classes.

@inproceedings{Sekerinski98GraphicalDesignReactiveSystem,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Graphical {Design} of {Reactive} {Systems}},
	volume = {1393},
	doi = {10.1007/BFb0053361},
	abstract = {Reactive systems can be designed graphically using statecharts. This paper presents a scheme for the translation of statecharts into the Abstract Machine Notation (AMN) of the B method. By an example of a conveyor system, we illustrate how the design can be initially expressed graphically with statecharts, then translated to AMN and analysed in AMN, and then further refined to executable code.},
	booktitle = {B'98: {Recent} {Advances} in the {Development} and {Use} of the {B} {Method}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Bert, Didier},
	month = apr,
	year = {1998},
	pages = {182--197},
}

Reactive systems can be designed graphically using statecharts. This paper presents a scheme for the translation of statecharts into the Abstract Machine Notation (AMN) of the B method. By an example of a conveyor system, we illustrate how the design can be initially expressed graphically with statecharts, then translated to AMN and analysed in AMN, and then further refined to executable code.

@inproceedings{MikhajlovSekerinski98FBCPImpact,
	address = {Jyväskylä, Finland},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {The {Fragile} {Base} {Class} {Problem} and {Its} {Impact} on {Component} {Systems}},
	volume = {1357},
	doi = {10.1007/3-540-69687-3_72},
	abstract = {In this paper we study applicability of the code inheritance mechanism to the domain of open component systems in light of so-called fragile base class problem. We propose a system architecture based on disciplined inheritance and present three check lists for component framework designers, component framework developers, and its users.},
	booktitle = {Object-{Oriented} {Technology}. {ECOOP} 1997},
	publisher = {Springer-Verlag},
	author = {Mikhajlov, Leonid and Sekerinski, Emil},
	editor = {Bosch, Jan and Mitchell, Stuart},
	year = {1998},
	pages = {353--358},
}

In this paper we study applicability of the code inheritance mechanism to the domain of open component systems in light of so-called fragile base class problem. We propose a system architecture based on disciplined inheritance and present three check lists for component framework designers, component framework developers, and its users.

@inproceedings{BuchiSekerinski98Components,
	address = {Jyväskylä, Finland},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Formal {Methods} for {Component} {Software}: {The} {Refinement} {Calculus} {Perspective}},
	volume = {1357},
	doi = {10.1007/3-540-69687-3_68},
	abstract = {We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Specifications using abstract statements scale up better than prepostconditions and allow for ‘relative’ specifications because they may refer to other components. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation of any component market.},
	booktitle = {Object-{Oriented} {Technology}. {ECOOP} 1997},
	publisher = {Springer-Verlag},
	author = {Büchi, Martin and Sekerinski, Emil},
	editor = {Bosch, Jan and Mitchell, Stuart},
	year = {1998},
	pages = {332--337},
}

We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Specifications using abstract statements scale up better than prepostconditions and allow for ‘relative’ specifications because they may refer to other components. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation of any component market.

@incollection{Sekerinski98ProductionCell,
	series = {Formal {Approaches} to {Computing} and {Information} {Technology} {Series}},
	title = {Production {Cell}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiSere98CaseStudiesB.pdf},
	abstract = {This chapter is about specifying and implementing a control program for a production cell using action systems in AMN. The production cell consists of five ma- chines: two conveyor belts, an elevating and rotating table, a two-arm robot, and a press. The machines are equipped with a total of 18 sensors for determining the positions of the machines and for sensing the transported plates and a total of eight actuators for setting the motors.
The production cell is a typical example of a discrete control system. In reality, all machines evolve continuously. However, at certain points the change of their state is notified to the control program, which may react to this change. Hence, the evolution of the system can be sufficiently represented as a sequence of steps. This means that discrete control systems can be modelled with (discrete) action systems. This chapter presents a general approach to developing control programs for discrete systems in AMN, and illustrates this with the complete development of a control program for a production cell.},
	booktitle = {Program {Development} by {Stepwise} {Refinement}: {Case} {Studies} {Using} the {B} {Method}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Sekerinski, Emil and Sere, Kaisa},
	year = {1998},
	doi = {10.1007/978-1-4471-0585-5_6},
	pages = {197--254},
}

This chapter is about specifying and implementing a control program for a production cell using action systems in AMN. The production cell consists of five ma- chines: two conveyor belts, an elevating and rotating table, a two-arm robot, and a press. The machines are equipped with a total of 18 sensors for determining the positions of the machines and for sensing the transported plates and a total of eight actuators for setting the motors. The production cell is a typical example of a discrete control system. In reality, all machines evolve continuously. However, at certain points the change of their state is notified to the control program, which may react to this change. Hence, the evolution of the system can be sufficiently represented as a sequence of steps. This means that discrete control systems can be modelled with (discrete) action systems. This chapter presents a general approach to developing control programs for discrete systems in AMN, and illustrates this with the complete development of a control program for a production cell.

@book{SekerinskiSere98CaseStudiesB,
	series = {Formal {Approaches} to {Computing} and {Information} {Technology}},
	title = {Program {Development} by {Stepwise} {Refinement}: {Case} {Studies} {Using} the {B} {Method}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiSere98CaseStudiesB.pdf},
	abstract = {The Idea of Program Refinement Programs are complex. They are typically so complex, that they go beyond the full comprehension even of the programmer or team who designed them, with all the consequences this has. How can we cope with such complexity in a satisfactory way? An approach, advocated for a long time, is to separate a concise specification of a program - the "what" - from a possibly involved implementation - the "how". Once a specification is obtained from the set of requirements on the program, there can still be a large gap to an efficient implementation. The development from specification to implementation can then proceed by a succession oflayers, such that each layer is a refinement of the previous one. Design decisions can be introduced in refinement steps one at a time. By this, the refinement steps can be kept small and manageable. Still, the set of all requirements can be far too large to be taken completely into account in the initial specification. Even if they could, they might obscure issues more than clarify them. For example: * An information system for stored goods needs to produce an error message on il- legal input. Yet, the exact wording - and even the language - of those messages is irrelevant for an understanding of the essence of the system. * A banking application interacts with customers with a graphical interface. Yet the specification of the graphical layout is secondary compared to the specification of the possible transactions.},
	publisher = {Springer-Verlag},
	editor = {Sekerinski, Emil and Sere, Kaisa},
	year = {1998},
	doi = {10.1007/978-1-4471-0585-5},
}

The Idea of Program Refinement Programs are complex. They are typically so complex, that they go beyond the full comprehension even of the programmer or team who designed them, with all the consequences this has. How can we cope with such complexity in a satisfactory way? An approach, advocated for a long time, is to separate a concise specification of a program - the "what" - from a possibly involved implementation - the "how". Once a specification is obtained from the set of requirements on the program, there can still be a large gap to an efficient implementation. The development from specification to implementation can then proceed by a succession oflayers, such that each layer is a refinement of the previous one. Design decisions can be introduced in refinement steps one at a time. By this, the refinement steps can be kept small and manageable. Still, the set of all requirements can be far too large to be taken completely into account in the initial specification. Even if they could, they might obscure issues more than clarify them. For example: * An information system for stored goods needs to produce an error message on il- legal input. Yet, the exact wording - and even the language - of those messages is irrelevant for an understanding of the essence of the system. * A banking application interacts with customers with a graphical interface. Yet the specification of the graphical layout is secondary compared to the specification of the possible transactions.

@inproceedings{MikhajlovaSekerinski97ClassInterfaceRefinement,
	address = {Graz, Austria},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Class {Refinement} and {Interface} {Refinement} in {Object}-{Oriented} {Programs}},
	volume = {1313},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/MikhajlovaSekerinski97ClassInterfaceRefinement.pdf},
	doi = {10.1007/3-540-63533-5_5},
	abstract = {Constructing new classes from existing ones by inheritance or subclassing is a characteristic feature of object-oriented development. Imposing semantic constraints on subclassing allows us to ensure that the behaviour of superclasses is preserved or refined in their subclasses. This paper defines a class refinement relation which captures these semantic constraints. The class refinement relation is based on algorithmic and data refinement supported by Refinement Calculus. Class refinement is generalized to interface refinement, which takes place when a change in user requirements causes interface changes of classes designed as refinements of other classes. We formalize the interface refinement relation and present rules for refinement of clients of the classes involved in this relation.},
	booktitle = {{FME} '97: {Industrial} {Applications} and {Strengthened} {Foundations} of {Formal} {Methods}},
	publisher = {Springer-Verlag},
	author = {Mikhajlova, Anna and Sekerinski, Emil},
	editor = {Fitzgerald, John and Jones, Cliff and Lucas, Peter},
	month = sep,
	year = {1997},
	pages = {82--101},
}

Constructing new classes from existing ones by inheritance or subclassing is a characteristic feature of object-oriented development. Imposing semantic constraints on subclassing allows us to ensure that the behaviour of superclasses is preserved or refined in their subclasses. This paper defines a class refinement relation which captures these semantic constraints. The class refinement relation is based on algorithmic and data refinement supported by Refinement Calculus. Class refinement is generalized to interface refinement, which takes place when a change in user requirements causes interface changes of classes designed as refinements of other classes. We formalize the interface refinement relation and present rules for refinement of clients of the classes involved in this relation.

@inproceedings{MikhajlovSekerinski97FBCPImpact,
	address = {Jyväskylä, Finland},
	series = {{TUCS} {General} {Publication}},
	title = {The {Fragile} {Base} {Class} {Problem} and {Its} {Impact} on {Component} {Systems}},
	volume = {5},
	url = {https://tucs.fi/publications/view/?pub_id=bWeBoSzy97},
	abstract = {In this paper we study applicability of the code inheritance mechanism to the domain of open component systems in light of so-called fragile base class problem. We present five requirements restricting code inheritance that are sufficient to circumvent the problem. We propose a system architecture based on disciplined inheritance and present three check lists for component framework designers, component framework developers, and its users.},
	booktitle = {Second {Workshop} on {Component}-{Oriented} {Programming} ({WCOP})},
	publisher = {Turku Centre for Computer Science},
	author = {Mikhajlov, Leonid and Sekerinski, Emil},
	editor = {Weck, Wolfgang and Bosch, Jan and Szyperski, Clemens},
	month = sep,
	year = {1997},
	pages = {59--68},
}

In this paper we study applicability of the code inheritance mechanism to the domain of open component systems in light of so-called fragile base class problem. We present five requirements restricting code inheritance that are sufficient to circumvent the problem. We propose a system architecture based on disciplined inheritance and present three check lists for component framework designers, component framework developers, and its users.

@inproceedings{BuchiSekerinski97Components,
	address = {Jyväskylä, Finland},
	series = {{TUCS} {General} {Publication}},
	title = {Formal {Methods} for {Component} {Software}: {The} {Refinement} {Calculus} {Perspective}},
	volume = {5},
	url = {https://tucs.fi/publications/view/?pub_id=bWeBoSzy97},
	abstract = {We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation for any component market.},
	booktitle = {Second {Workshop} on {Component}-{Oriented} {Programming} ({WCOP})},
	publisher = {Turku Centre for Computer Science},
	author = {Büchi, Martin and Sekerinski, Emil},
	editor = {Weck, Wolfgang and Bosch, Jan and Szyperski, Clemens},
	month = sep,
	year = {1997},
	pages = {23--32},
}

We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation for any component market.

@techreport{MikhajlovSekerinski97FBCPSolution,
	type = {{TUCS} {Technical} {Report}},
	title = {The {Fragile} {Base} {Class} {Problem} and {Its} {Solution}},
	url = {http://tucs.fi/publications/view/?pub_id=tLMiSe97},
	abstract = {In this paper, we study the fragile base class problem. This problem occurs in open object-oriented systems employing code inheritance as an implementation reuse mechanism. System developers unaware of extensions to the system developed by its users may produce a seemingly acceptable revision of a base class which may damage its extensions. The fragile base class problem becomes apparent during maintenance of open object-oriented systems but requires consideration during design. We formulate the fragile base class problem in terms of a flexibility property. By means of five orthogonal examples demonstrating that the flexibility property does not hold, we introduce requirements for disciplining inheritance. We extend the refinement calculus to accommodate for classes, objects, class-based inheritance, and class refinement. We formulate and formally prove a flexibility theorem showing that the restrictions we impose on inheritance are sufficient to permit substituting a base class with its revision in the presence of extension classes. We also present three checklists for system designers, developers, and extenders to allow application of our results in practice informally.},
	number = {117},
	institution = {Turku Centre for Computer Science},
	author = {Mikhajlov, Leonid and Sekerinski, Emil},
	month = may,
	year = {1997},
	keywords = {ISBN 952-12-0020-0 ISSN 1239-1891 32 pages},
	pages = {34},
}

In this paper, we study the fragile base class problem. This problem occurs in open object-oriented systems employing code inheritance as an implementation reuse mechanism. System developers unaware of extensions to the system developed by its users may produce a seemingly acceptable revision of a base class which may damage its extensions. The fragile base class problem becomes apparent during maintenance of open object-oriented systems but requires consideration during design. We formulate the fragile base class problem in terms of a flexibility property. By means of five orthogonal examples demonstrating that the flexibility property does not hold, we introduce requirements for disciplining inheritance. We extend the refinement calculus to accommodate for classes, objects, class-based inheritance, and class refinement. We formulate and formally prove a flexibility theorem showing that the restrictions we impose on inheritance are sufficient to permit substituting a base class with its revision in the presence of extension classes. We also present three checklists for system designers, developers, and extenders to allow application of our results in practice informally.

@inproceedings{BackBuchiSekerinski97ActionBasedObjects,
	address = {Palma, Mallorca, Spain},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Action-{Based} {Concurrency} and {Synchronization} for {Objects}},
	volume = {1231},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/BackBuchiSekerinski97ActionBasedObjects.pdf},
	doi = {10.1007/3-540-63010-4_17},
	abstract = {We extend the Action-Oberon language for executing action systems with type-bound actions. Type-bound actions combine the concepts of type-bound procedures (methods) and actions, bringing object orientation to action systems. Type-bound actions are created at runtime along with the objects of their bound types. They permit the encapsulation of data and code in objects. Allowing an action to have more than one participant gives us a mechanism for expressing n-ary communication between objects. By showing how type-bound actions can logically be reduced to plain actions, we give our extension a firm foundation in the Refinement Calculus.},
	booktitle = {Transformation-{Based} {Reactive} {System} {Development}, {Fourth} {AMAST} {Workshop} on {Real}-{Time} {Systems}, {Concurrent}, and {Distributed} {Software}},
	publisher = {Springer-Verlag},
	author = {Back, Ralph and Büchi, Martin and Sekerinski, Emil},
	editor = {Rus, T. and Bertran, M.},
	month = may,
	year = {1997},
	pages = {248--262},
}

We extend the Action-Oberon language for executing action systems with type-bound actions. Type-bound actions combine the concepts of type-bound procedures (methods) and actions, bringing object orientation to action systems. Type-bound actions are created at runtime along with the objects of their bound types. They permit the encapsulation of data and code in objects. Allowing an action to have more than one participant gives us a mechanism for expressing n-ary communication between objects. By showing how type-bound actions can logically be reduced to plain actions, we give our extension a firm foundation in the Refinement Calculus.

@techreport{MikhajlovaSekerinski97ClassInterfaceRefinementReport,
	type = {{TUCS} {Technical} {Report}},
	title = {Class {Refinement} and {Interface} {Refinement} in {Object}-{Oriented} {Development}},
	url = {http://tucs.fi/publications/view/?pub_id=tMiSe97},
	institution = {Turku Centre for Computer Science},
	author = {Mikhajlova, Anna and Sekerinski, Emil},
	month = mar,
	year = {1997},
	pages = {10},
}

@misc{SekerinskiSereTroubitsyna96ProbabilitiesActionSystems,
	address = {Oslo, Norway},
	title = {Probabilities in {Action} {Systems}},
	url = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no/~nwpt96/},
	abstract = {Action systems combined with the refinement calculus {\textbackslash}citeBaKu83,BaSe94:FME is a powerful tool for the design of parallel and distributed systems in a stepwise manner. The basic idea behind action systems is that actions are atomic entities that are chosen for execution nondeterministically. In many situations, especially when designing of control systems {\textbackslash}citeBuSS96, some preliminary information regarding probabilities of execution of certain actions is given. Within action systems we cannot take this information into account and hence we get only a pessimistic estimation of system behavior. The formalism is based on the predicate transformer semantics. Recently the notion of probabilistic predicate transformers has been introduced {\textbackslash}citeMorg96 to reason about probabilistic behavior of programs as well as refinement. We propose a way of combining the probabilistic predicate transformer theory with the action systems formalism and identify a class of action systems where such merging is possible. We {\textbackslash}em embed a probabilistic actions, i.e. actions where a choice of action is performed probabilistically, into a nondeterministic action system. Thus in a probabilistic action system some of the nondeterministic choices are replaced by probabilistic choices. We show that the introduction of probabilistic action systems still allows us to perform refinement of action systems in an ordinary way. Thus we can reason about the correctness of probabilistic tasks within the refinement calculus for action systems. {\textbackslash}bibitemBaKu83 R. J. R. Back and R. Kurki-Suonio. {\textbackslash}newblock Decentralization of process nets with centralized control. {\textbackslash}newblock In {\textbackslash}em Proc.{\textbackslash} of the 2nd ACM SIGACT–SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983. {\textbackslash}bibitemBaSe94:FME R. J. R. Back and K. Sere. {\textbackslash}newblock From modular systems to action systems. {\textbackslash}newblock Proc.{\textbackslash} of {\textbackslash}em Formal Methods Europe'94, Spain, October 1994. {\textbackslash}newblock {\textbackslash}em Lecture Notes in Computer Science. Springer–Verlag, 1994. {\textbackslash}bibitemBuSS96 M. Butler, E. Sekerinski, and K. Sere. An Action System Approach to the Steam Boiler Problem. In Jean-Raymond Abrial, Egon Borger and Hans Langmaack, editors, {\textbackslash}em Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science Vol. 1165. Springer-Verlag, 1996. To appear. {\textbackslash}bibitemMorg96 K. Seidel, C.C. Morgan and A.K. McIver. {\textbackslash}newblock An introduction to probabilistic predicate transformers. {\textbackslash}newblock {\textbackslash}em Technical report PRG-TR-6-96, Programming Research Group, 1996.},
	author = {Sekerinski, Emil and Sere, Kaisa and Troubitsyna, Elena},
	month = dec,
	year = {1996},
}

Action systems combined with the refinement calculus \citeBaKu83,BaSe94:FME is a powerful tool for the design of parallel and distributed systems in a stepwise manner. The basic idea behind action systems is that actions are atomic entities that are chosen for execution nondeterministically. In many situations, especially when designing of control systems \citeBuSS96, some preliminary information regarding probabilities of execution of certain actions is given. Within action systems we cannot take this information into account and hence we get only a pessimistic estimation of system behavior. The formalism is based on the predicate transformer semantics. Recently the notion of probabilistic predicate transformers has been introduced \citeMorg96 to reason about probabilistic behavior of programs as well as refinement. We propose a way of combining the probabilistic predicate transformer theory with the action systems formalism and identify a class of action systems where such merging is possible. We \em embed a probabilistic actions, i.e. actions where a choice of action is performed probabilistically, into a nondeterministic action system. Thus in a probabilistic action system some of the nondeterministic choices are replaced by probabilistic choices. We show that the introduction of probabilistic action systems still allows us to perform refinement of action systems in an ordinary way. Thus we can reason about the correctness of probabilistic tasks within the refinement calculus for action systems. \bibitemBaKu83 R. J. R. Back and R. Kurki-Suonio. \newblock Decentralization of process nets with centralized control. \newblock In \em Proc.\ of the 2nd ACM SIGACT–SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983. \bibitemBaSe94:FME R. J. R. Back and K. Sere. \newblock From modular systems to action systems. \newblock Proc.\ of \em Formal Methods Europe'94, Spain, October 1994. \newblock \em Lecture Notes in Computer Science. Springer–Verlag, 1994. \bibitemBuSS96 M. Butler, E. Sekerinski, and K. Sere. An Action System Approach to the Steam Boiler Problem. In Jean-Raymond Abrial, Egon Borger and Hans Langmaack, editors, \em Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science Vol. 1165. Springer-Verlag, 1996. To appear. \bibitemMorg96 K. Seidel, C.C. Morgan and A.K. McIver. \newblock An introduction to probabilistic predicate transformers. \newblock \em Technical report PRG-TR-6-96, Programming Research Group, 1996.

@misc{MikhailovaSekerinski96ClassInterfaceRefinement,
	address = {Oslo, Norway},
	title = {Class {Refinement} and {Interface} {Refinement} in {Object}-{Oriented} {Development}},
	url = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no:80/~nwpt96/},
	author = {Mikhajlova, Anna and Sekerinski, Emil},
	month = dec,
	year = {1996},
}

@misc{BackMikhailovSekerinski96FormalDesignPatterns,
	address = {Oslo, Norway},
	title = {Formal {Description} of {Object}-{Oriented} {Design} {Patterns}},
	url = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no:80/~nwpt96/},
	abstract = {This paper addresses the issue of specifying Object-Oriented Design Patterns [1] formally. Object-Oriented Design Patterns document an expertise in the field of OO Design. They describe simple and elegant solutions to concrete problems. Usually the patterns are presented informally, thus many subtle issues remain unclear and underspecified. In particular, relations among the participants of the patterns are rather obscure. We use the formal semantics and the notation of the object-oriented programming and specification language developed in [2]. The advantage of this approach is the uniform way of presenting all stages of development starting with an abstract specification of general system architecture and ending with a concrete executable program. This allows for specifying patterns and custom designs following them in the same terms and simplifies reasoning about their interrelations. A characteristic feature of the used formalism is the distinction between classes and object types. This entitles us to be precise about the relationship among entities participating in a pattern. For example, very often the conformance of the class interfaces (i.e. object types) is insufficient to precisely specify a pattern. In this case we can require that classes are in the refinement relation [3]. Most of the patterns promote clear and extendable design. It means that the program following a pattern will be easily extendable along some axes and very rigid along the others. With the informal specifications such issues are not immediately apparent. The described approach allows for indicating clearly hot spots [4]. (i.e places intended for future extensions) and frozen spots. This is achieved using a mechanism of parameterization of classes with types, values and other classes available in the formalism. References [1] Erich Gamma, Richard Helm, Ralph Johnson, John Vlissides Design Patterns. ADDISON-WESLEY, ( May 1994). [2] Emil Sekerinski A Type-Theoretic Basis for an Object-Oriented Refinement Calculus. Dept. of Computer Science, Abo Akademi, Turku, Finland [3] R.J.R. Back Correctness Preserving Program Refinements:Proof Theory and Applications vol. 131 of Mathematical Center Tracts. Amsterdam: Mathematical Center 1980 [4] Wolfgang Pree Design Patterns for Object-Oriented Software Development ADDISON-WESLEY,1994.},
	author = {Back, Ralph and Mikhajlov, Leonid and Sekerinski, Emil},
	month = dec,
	year = {1996},
}

This paper addresses the issue of specifying Object-Oriented Design Patterns [1] formally. Object-Oriented Design Patterns document an expertise in the field of OO Design. They describe simple and elegant solutions to concrete problems. Usually the patterns are presented informally, thus many subtle issues remain unclear and underspecified. In particular, relations among the participants of the patterns are rather obscure. We use the formal semantics and the notation of the object-oriented programming and specification language developed in [2]. The advantage of this approach is the uniform way of presenting all stages of development starting with an abstract specification of general system architecture and ending with a concrete executable program. This allows for specifying patterns and custom designs following them in the same terms and simplifies reasoning about their interrelations. A characteristic feature of the used formalism is the distinction between classes and object types. This entitles us to be precise about the relationship among entities participating in a pattern. For example, very often the conformance of the class interfaces (i.e. object types) is insufficient to precisely specify a pattern. In this case we can require that classes are in the refinement relation [3]. Most of the patterns promote clear and extendable design. It means that the program following a pattern will be easily extendable along some axes and very rigid along the others. With the informal specifications such issues are not immediately apparent. The described approach allows for indicating clearly hot spots [4]. (i.e places intended for future extensions) and frozen spots. This is achieved using a mechanism of parameterization of classes with types, values and other classes available in the formalism. References [1] Erich Gamma, Richard Helm, Ralph Johnson, John Vlissides Design Patterns. ADDISON-WESLEY, ( May 1994). [2] Emil Sekerinski A Type-Theoretic Basis for an Object-Oriented Refinement Calculus. Dept. of Computer Science, Abo Akademi, Turku, Finland [3] R.J.R. Back Correctness Preserving Program Refinements:Proof Theory and Applications vol. 131 of Mathematical Center Tracts. Amsterdam: Mathematical Center 1980 [4] Wolfgang Pree Design Patterns for Object-Oriented Software Development ADDISON-WESLEY,1994.

@misc{BackMikhailovaSekerinski96StepwiseInterfaceRefinement,
	address = {Oslo, Norway},
	title = {Stepwise {Development} of {Object}-{Oriented} {Programs} with {Interface} {Refinement}},
	url = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no:80/~nwpt96/},
	author = {Back, R. J. and Mikhaljova, A. and Sekerinski, E.},
	month = dec,
	year = {1996},
}

@techreport{BackBuchiSekerinski96TypeBoundActions,
	type = {{TUCS} {Technical} {Report}},
	title = {Adding {Type}-{Bound} {Actions} to {Action}-{Oberon}},
	url = {https://tucs.fi/publications/view/?pub_id=tBaBuSe96},
	abstract = {We extend the Action-Oberon language for executing action systems with type-bound actions. Type-bound actions combine the concepts of type-bound procedures (methods) and actions, bringing object orientation to action systems. Type-bound actions are created at runtime along with the objects of their bound types. They permit the encapsulation of data and code in objects. Allowing an action to have more than one participant gives us a mechanism for expressing n-ary communication between objects. By showing how type-bound actions can logically be reduced to plain actions, we give our extension a firm foundation in the Refinement Calculus.},
	number = {66},
	institution = {Turku Centre for Computer Science},
	author = {Back, Ralph and Büchi, Martin and Sekerinski, Emil},
	month = nov,
	year = {1996},
	pages = {15},
}

We extend the Action-Oberon language for executing action systems with type-bound actions. Type-bound actions combine the concepts of type-bound procedures (methods) and actions, bringing object orientation to action systems. Type-bound actions are created at runtime along with the objects of their bound types. They permit the encapsulation of data and code in objects. Allowing an action to have more than one participant gives us a mechanism for expressing n-ary communication between objects. By showing how type-bound actions can logically be reduced to plain actions, we give our extension a firm foundation in the Refinement Calculus.

@inproceedings{ButlerSekerinskiSere96SteamBoiler,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {An {Action} {System} {Approach} to the {Steam} {Boiler} {Problem}},
	volume = {1165},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/ButlerSekerinskiSere96SteamBoiler.pdf},
	doi = {10.1007/BFb0027234},
	abstract = {This paper presents an approach to the specification of control programs based on action systems and refinement. The system to be specified and its physical environment are first modelled as one initial action system. This allows us to abstract away from the communication mechanism between the two entities. It also allows us to state and use clearly the assumptions that we make about how the environment behaves. In subsequent steps the specifications of control program and the environment are further elaborated by refinement and are separated. We use the refinement calculus to structure and reason about the specification. The operators in this calculus allow us to achieve a high degree of modularity in the development.},
	booktitle = {Formal {Methods} for {Industrial} {Applications}: {Specifying} and {Programming} the {Steam} {Boiler} {Control}},
	publisher = {Springer-Verlag},
	author = {Butler, Michael and Sekerinski, Emil and Sere, Kaisa},
	editor = {Abrial, Jean-Raymond and Börger, Egon and Langmaack, Hans},
	month = oct,
	year = {1996},
	pages = {129--148},
}

This paper presents an approach to the specification of control programs based on action systems and refinement. The system to be specified and its physical environment are first modelled as one initial action system. This allows us to abstract away from the communication mechanism between the two entities. It also allows us to state and use clearly the assumptions that we make about how the environment behaves. In subsequent steps the specifications of control program and the environment are further elaborated by refinement and are separated. We use the refinement calculus to structure and reason about the specification. The operators in this calculus allow us to achieve a high degree of modularity in the development.

@inproceedings{RonkkoSekerinskiSere96ControlActionSystems,
	address = {Edinburgh},
	title = {Control {Systems} as {Action} {Systems}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/RonkkoSekerinskiSere96ControlActionSystems.pdf},
	abstract = {We study the problem of constructing controllers for discrete event systems using the action systems formalism. Action systems are based on predicate transformers where the state base of the system is of utmost importance. There are no notions of events or alphabet sets that are used in many other approaches. Action systems have proved their worth in many applications, typically when modelling different types of concurrent behaviour. We outline an action systems based approach to constructing a controller for a discrete event system and apply it to an example of a practical, real-world control problem. We show how the important safety properties can be proved within this framework.},
	booktitle = {{WODES} 96 – {Workshop} on {Discrete} {Event} {Systems}},
	publisher = {Institute of Electronical Engineers},
	author = {Rönkkö, Mauno and Sekerinski, Emil and Sere, Kaisa},
	editor = {Smedinga, R. and Spathopoulos, M. P. and Kozák, P.},
	month = aug,
	year = {1996},
	pages = {362--367},
}

We study the problem of constructing controllers for discrete event systems using the action systems formalism. Action systems are based on predicate transformers where the state base of the system is of utmost importance. There are no notions of events or alphabet sets that are used in many other approaches. Action systems have proved their worth in many applications, typically when modelling different types of concurrent behaviour. We outline an action systems based approach to constructing a controller for a discrete event system and apply it to an example of a practical, real-world control problem. We show how the important safety properties can be proved within this framework.

@article{SekerinskiSere96PrioritizingComposition,
	title = {A {Theory} of {Prioritizing} {Composition}},
	volume = {39},
	doi = {10.1093/comjnl/39.8.701},
	abstract = {An operator for the composition of two processes, where one process has priority over the other process, is studied. Processes are described by action systems, and data refinement is used for transforming processes. The operator is shown to be compositional, i.e. monotonic with respect to refinement. It is argued that this operator is adequate for modelling priorities as found in programming languages and operating systems. Rules for introducing priorities and for raising and lowering priorities of processes are given. Dynamic priorities are modelled with special priority variables which can be freely mixed with other variables and the prioritizing operator in program development. A number of applications show the use of prioritizing composition for modelling and specification in general.},
	number = {8},
	journal = {The Computer Journal},
	author = {Sekerinski, Emil and Sere, Kaisa},
	month = aug,
	year = {1996},
	pages = {701--712},
}

An operator for the composition of two processes, where one process has priority over the other process, is studied. Processes are described by action systems, and data refinement is used for transforming processes. The operator is shown to be compositional, i.e. monotonic with respect to refinement. It is argued that this operator is adequate for modelling priorities as found in programming languages and operating systems. Rules for introducing priorities and for raising and lowering priorities of processes are given. Dynamic priorities are modelled with special priority variables which can be freely mixed with other variables and the prioritizing operator in program development. A number of applications show the use of prioritizing composition for modelling and specification in general.

@techreport{SekerinskiSere96PrioritisingCompositionReport,
	type = {{TUCS} {Technical} {Report}},
	title = {A {Theory} of {Prioritising} {Composition}},
	url = {https://tucs.fi/publications/view/?pub_id=tSS96},
	abstract = {An operator for the composition of two processes, where one process has priority over the other process, is studied. Processes are described by action systems, and data refinement is used for transforming processes. The operator is shown to be compositional, i.e. monotonic with respect to refinement. It is argued that this operator is adequate for modelling priorities as found in programming languages and operating systems. Rules for introducing priorities and for raising and lowering priorities of processes are given. Dynamic priorities are modelled with special priority variables which can be freely mixed with other variables and the prioritising operator in program development. A number of applications show the use of prioritising composition for modelling and specification in general.},
	number = {5},
	institution = {Turku Centre for Computer Science},
	author = {Sekerinski, Emil and Sere, Kaisa},
	month = may,
	year = {1996},
	pages = {23},
}

An operator for the composition of two processes, where one process has priority over the other process, is studied. Processes are described by action systems, and data refinement is used for transforming processes. The operator is shown to be compositional, i.e. monotonic with respect to refinement. It is argued that this operator is adequate for modelling priorities as found in programming languages and operating systems. Rules for introducing priorities and for raising and lowering priorities of processes are given. Dynamic priorities are modelled with special priority variables which can be freely mixed with other variables and the prioritising operator in program development. A number of applications show the use of prioritising composition for modelling and specification in general.

@techreport{Sekerinski96ControlProgramWeakestPreconditions,
	type = {{TUCS} {Technical} {Report}},
	title = {Deriving {Control} {Programs} by {Weakest} {Preconditions}},
	url = {http://tucs.fi/publications/view/?pub_id=tSekerinski96},
	abstract = {A control program is understood as a reactive component that maintains a continuous interaction with its environment. A formal criterion for the correctness of a control program is given. This criterion can be applied in reverse for deriving a control program from properties of the whole control system. This is illustrated by an example of two conveyor belts. The formal reasoning is based on the weakest precondition calculus. Action systems are used for modelling the control system.},
	number = {4},
	institution = {Turku Centre for Computer Science},
	author = {Sekerinski, Emil},
	month = apr,
	year = {1996},
	pages = {21},
}

A control program is understood as a reactive component that maintains a continuous interaction with its environment. A formal criterion for the correctness of a control program is given. This criterion can be applied in reverse for deriving a control program from properties of the whole control system. This is illustrated by an example of two conveyor belts. The formal reasoning is based on the weakest precondition calculus. Action systems are used for modelling the control system.

@incollection{Sekerinski96TypeTheoreticObjectOrientedRefinement,
	title = {A {Type}-{Theoretic} {Basis} for an {Object}-{Oriented} {Refinement} {Calculus}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski96TypeTheoreticObjectOrientedRefinement.pdf},
	abstract = {This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes. The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes. The semantics is given by a translation of the constructs into the type system F≤, an extension of the simple typed λ-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers, i. e. higher order functions mapping state predicates (postconditions) to state predicates (preconditions). Objects are represented by records of statements (the methods) operating on a record of attributes, where the attributes are hidden by existential quantification. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism, e. g. for the parameterization of classes by types, are already present in F≤. The advantage of this semantic by translation is that it builds on the features already provided by F≤ (which are all used). Hence no direct reference to the model underlying F≤ needs to be made; a summary of the syntax and rules of F≤ is given.},
	booktitle = {Formal {Methods} and {Object} {Technology}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Goldsack, Stephen J. and Kent, Stuart J. H.},
	year = {1996},
	doi = {10.1007/978-1-4471-3071-0_15},
	keywords = {10.1007/978-1-4471-3071-0\_15},
	pages = {317--335},
}

This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes. The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes. The semantics is given by a translation of the constructs into the type system F≤, an extension of the simple typed λ-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers, i. e. higher order functions mapping state predicates (postconditions) to state predicates (preconditions). Objects are represented by records of statements (the methods) operating on a record of attributes, where the attributes are hidden by existential quantification. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism, e. g. for the parameterization of classes by types, are already present in F≤. The advantage of this semantic by translation is that it builds on the features already provided by F≤ (which are all used). Hence no direct reference to the model underlying F≤ needs to be made; a summary of the syntax and rules of F≤ is given.

@inproceedings{ButlerSekerinskiSere95SteamBoilerDagstuhl,
	address = {Dagstuhl, Germany},
	series = {Dagstuhl {Seminiar}-{Report}},
	title = {An {Action} {System} {Approach} to the {Steam} {Boiler} {Problem}},
	volume = {117},
	url = {http://www.dagstuhl.de/9523},
	booktitle = {Methods for {Semantics} and {Specification}},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany},
	author = {Butler, Michael and Sekerinski, Emil and Sere, Kaisa},
	editor = {Abrial, J.-R. and Börger, E. and Langmaack, H.},
	month = jun,
	year = {1995},
	pages = {1 -- 5},
}

@techreport{ButlerSekerinskiSere95SteamBoiler,
	type = {{TUCS} {Technical} {Report}},
	title = {An {Action} {System} {Approach} to the {Steam} {Boiler} {Problem}},
	url = {http://tucs.fi/publications/view/?pub_id=tBuSeSe95},
	abstract = {This paper presents an approach to the specification of control programs based on action systems and refinement. The system to be specified and its physical environment are first modelled as one initial action system. This allows us to abstract away from the communication mechanism between the two entities. It also allows us to state and use clearly the assumptions that we make about how the environment behaves. In subsequent steps the specifications of control program and the environment are further elaborated by refinement and are separated. We use the refinement calculus to structure and reason about the specification. The operators in this calculus allow us to achieve a high degree of modularity in the development. An important aim of this paper is to produce an action system specification of the Steam Boiler problem.},
	institution = {Turku Centre for Computer Science},
	author = {Butler, Michael and Sekerinski, Emil and Sere, Kaisa},
	year = {1995},
	pages = {29},
}

This paper presents an approach to the specification of control programs based on action systems and refinement. The system to be specified and its physical environment are first modelled as one initial action system. This allows us to abstract away from the communication mechanism between the two entities. It also allows us to state and use clearly the assumptions that we make about how the environment behaves. In subsequent steps the specifications of control program and the environment are further elaborated by refinement and are separated. We use the refinement calculus to structure and reason about the specification. The operators in this calculus allow us to achieve a high degree of modularity in the development. An important aim of this paper is to produce an action system specification of the Steam Boiler problem.

@incollection{LewerentzLindnerRupingSekerinski95OODesignVerification,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {On {Object}-{Oriented} {Design} and {Verification}},
	volume = {1009},
	abstract = {We present a theory of object-orientation on the basis of the refinement calculus. This theory allows for specifying the behaviour of objects and provides a calculus for the proof of relationships between classes such as refinement. Given two similar, but not identical classes, we present an algorithm to construct a common superclass which is refined by both classes, and an algorithm to construct a common subclass which refines both classes. As an example, we present an account manager to illustrate design and verification. The overall approach aims at giving a simple theoretical basis for incremental object-oriented software construction. We demonstrate how formal specification and verification can be integrated into the development process, and thus can be put into practical use.},
	booktitle = {{KORSO}: {Methods}, {Languages}, and {Tools} for the {Construction} of {Correct} {Software}},
	publisher = {Springer-Verlag},
	author = {Lewerentz, C. and Lindner, T. and Rüping, A. and Sekerinski, E.},
	editor = {Broy, Manfred and Jähnichen, Stefan},
	year = {1995},
	doi = {10.1007/BFb0015457},
	pages = {92--111},
}

We present a theory of object-orientation on the basis of the refinement calculus. This theory allows for specifying the behaviour of objects and provides a calculus for the proof of relationships between classes such as refinement. Given two similar, but not identical classes, we present an algorithm to construct a common superclass which is refined by both classes, and an algorithm to construct a common subclass which refines both classes. As an example, we present an account manager to illustrate design and verification. The overall approach aims at giving a simple theoretical basis for incremental object-oriented software construction. We demonstrate how formal specification and verification can be integrated into the development process, and thus can be put into practical use.

@incollection{ErasmySekerinski95RAISE,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {{RAISE}: {A} {Rigorous} {Approach} {Using} {Stepwise} {Refinement}},
	volume = {891},
	abstract = {We present the process-oriented RAISE contribution, beginning with a short presentation of the RAISE method, tools, and specification language. Then we show how the production cell software is developed using a rigorous approach with successive refinements of the specification. We present extracts from the production cell specifications. Finally, we give an evaluation of the RAISE contribution: the properties that could be specified and proved, the assumptions made, the flexibility of the specifications and proofs and some measures concerning them.},
	booktitle = {Formal {Development} of {Reactive} {Systems} – {Case} {Study} {Production} {Cell}},
	publisher = {Springer-Verlag},
	author = {Erasmy, F. and Sekerinski, E.},
	editor = {Lewerentz, C. and Lindner, Th.},
	year = {1995},
	doi = {10.1007/3-540-58867-1_60},
	pages = {277--293},
}

We present the process-oriented RAISE contribution, beginning with a short presentation of the RAISE method, tools, and specification language. Then we show how the production cell software is developed using a rigorous approach with successive refinements of the specification. We present extracts from the production cell specifications. Finally, we give an evaluation of the RAISE contribution: the properties that could be specified and proved, the assumptions made, the flexibility of the specifications and proofs and some measures concerning them.

@incollection{RupingSekerinski95Modula3,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Modula-3: {Modelling} and {Implementation}},
	volume = {891},
	abstract = {We present the modelling, implementation, and verification of a software system for the control of an industrial production cell. We use techniques of object-oriented and of parallel programming for both modelling and implementation. The implementation is done in Modula-3. We demonstrate the verification of safety requirements for the production cell. We discuss how well Modula-3 is suited for developing the control software in this case study. In detail, we analyse the benefits of object-oriented and parallel constructs and how both can be integrated with each other.},
	booktitle = {Formal {Development} of {Reactive} {Systems} - {Case} {Study} {Production} {Cell}},
	publisher = {Springer-Verlag},
	author = {Rüping, A. and Sekerinski, E.},
	editor = {Lewerentz, C. and Lindner, Th.},
	year = {1995},
	doi = {10.1007/3-540-58867-1_64},
	pages = {357--371},
}

We present the modelling, implementation, and verification of a software system for the control of an industrial production cell. We use techniques of object-oriented and of parallel programming for both modelling and implementation. The implementation is done in Modula-3. We demonstrate the verification of safety requirements for the production cell. We discuss how well Modula-3 is suited for developing the control software in this case study. In detail, we analyse the benefits of object-oriented and parallel constructs and how both can be integrated with each other.

@incollection{LewerentzLindnerRupingSekerinski95OODesignVerificationReport,
	title = {On {Object}-{Oriented} {Design} and {Verification}},
	volume = {1},
	booktitle = {Architectures and {Processes} for {Systematic} {Software} {Construction}},
	publisher = {FZI Publication},
	author = {Lewerentz, C. and Lindner, T. and Rüping, A. and Sekerinski, E.},
	editor = {Casais, E.},
	year = {1995},
	pages = {27--51},
}

@inproceedings{erasmy_stepwise_1994,
	address = {Barcelona, Spain},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Stepwise {Refinement} of {Control} {Software} - {A} {Case} {Study} using {RAISE}},
	volume = {873},
	doi = {10.1007/3-540-58555-9_115},
	booktitle = {{FME}'94: {Industrial} {Benefit} of {Formal} {Methods}},
	publisher = {Springer-Verlag},
	author = {Erasmy, F. and Sekerinski, E.},
	editor = {Naftalin, M. and Denvir, T. and Bertran, M.},
	month = oct,
	year = {1994},
	note = {CitationKey: ErasmySekerinski94ControlRefinement},
	pages = {547--566},
}

@incollection{RupingSekerinski95Modula3Report,
	title = {Modula-3: {The} {Modelling} and {Implementation} of an {Industrial} {Production} {Cell}},
	volume = {1},
	booktitle = {Case {Study} {Production} {Cell} - {A} {Comparative} {Study} in {Formal} {Software} {Development}},
	publisher = {FZI Publication},
	author = {Rüping, A. and Sekerinski, E.},
	editor = {Lewerentz, C. and Lindner, Th.},
	year = {1994},
	pages = {357--371},
}

@incollection{ErasmySekerinski95RAISE,
	title = {{RAISE}: {A} {Rigorous} {Approach} {Towards} the {Production} {Cell} {Using} {Stepwise} {Refinement}},
	volume = {1},
	booktitle = {Case {Study} “{Production} {Cell}”—{A} {Comparative} {Study} in {Formal} {Software} {Development}},
	publisher = {FZI Publication},
	author = {Erasmy, F. and Sekerinski, E.},
	editor = {Lewerentz, C. and Lindner, Th.},
	year = {1994},
	pages = {155--172},
}

@phdthesis{Sekerinski94VerfeinerungOOP,
	type = {Dissertation},
	title = {Verfeinerung in der {Objektorientierten} {Programmkonstruktion}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski94VerfeinerungOOP.pdf},
	abstract = {Die vorliegende Arbeit gibt eine formale Fundierung objektorientierter Entwurfsprinzipien. Hierzu wird eine Notation definiert, die zum einen alle wesentlichen Elemente objektorientierter Programmiersprachen enthält, und zum anderen Spezifikationskonstrukte bietet. In dieser Notation werden folgende typische objektorientierte Entwurfsprinzipien betrachtet:
• Implementieren von Klassen
• Inkrementelles Modifizieren von Klassen durch Vererbung
• Herausfaktorisieren von Gemeinsamkeiten von Klassen
Es werden Beweis- und Konstruktionsregeln für die korrekte Anwendung dieser Entwurfsprinzipien aufgestellt. Die Regeln tragen auch zu einem tieferen Verständnis der Entwurfsprinzipien bei.
Spezifikationen haben die Form von indeterministischen Anweisungen, wie sie
aus dem Verfeinerungskalkül bekannt sind, bei denen das Resultat durch ein
Prädikat spezifiziert wird. An objektorientierten Konzepten werden Objekte mit
Attributen und Methoden, Kapselung privater Attribute, Klassen mit Vererbung,
Untertyp-Polymorphie, parametrische Polymorphie und Objektidentitäten betrachtet. Für die Semantik der Notation wird das Typsystem Fω≤, eine Erweiterung des typisierten λ-Kalküls, zugrunde gelegt. Anweisungen werden durch Prädikatentransformer definiert. Damit wird gezeigt, wie eine Notation, die bezüglich der Spezifikationsmächtigkeit und der Flexibilität der Typisierung über existierende typisierte objektorientierte Programmier- und Spezifikationssprachen hinausgeht, formal definiert werden kann. Die Flexibilität beruht insbesondere auf der Unterscheidung von Objekttypen und Klassen.
Das zentrale methodische Konzept ist die Klassenverfeinerung. Sie erlaubt es, abstrakte, spezifizierende Klassen durch konkretere, implementierungsnähere zu ersetzen. Es wird gezeigt, daß Klassenverfeinerung durch die aus dem Verfeinerungskalkül bekannte Technik der Datenverfeinerung nachgewiesen werden kann. Für die Verfeinerung von inkrementell modifizierten Klassen werden spezielle, vereinfachte Beweisregeln aufgestellt. Das Herausfaktorisieren von Gemeinsamkeiten von Klassen wird durch zwei neuartige Operatoren, Klassenschnitt und Klassenvereinigung, unterstützt.},
	school = {University of Karlsruhe},
	author = {Sekerinski, Emil},
	year = {1994},
}

Die vorliegende Arbeit gibt eine formale Fundierung objektorientierter Entwurfsprinzipien. Hierzu wird eine Notation definiert, die zum einen alle wesentlichen Elemente objektorientierter Programmiersprachen enthält, und zum anderen Spezifikationskonstrukte bietet. In dieser Notation werden folgende typische objektorientierte Entwurfsprinzipien betrachtet: • Implementieren von Klassen • Inkrementelles Modifizieren von Klassen durch Vererbung • Herausfaktorisieren von Gemeinsamkeiten von Klassen Es werden Beweis- und Konstruktionsregeln für die korrekte Anwendung dieser Entwurfsprinzipien aufgestellt. Die Regeln tragen auch zu einem tieferen Verständnis der Entwurfsprinzipien bei. Spezifikationen haben die Form von indeterministischen Anweisungen, wie sie aus dem Verfeinerungskalkül bekannt sind, bei denen das Resultat durch ein Prädikat spezifiziert wird. An objektorientierten Konzepten werden Objekte mit Attributen und Methoden, Kapselung privater Attribute, Klassen mit Vererbung, Untertyp-Polymorphie, parametrische Polymorphie und Objektidentitäten betrachtet. Für die Semantik der Notation wird das Typsystem Fω≤, eine Erweiterung des typisierten λ-Kalküls, zugrunde gelegt. Anweisungen werden durch Prädikatentransformer definiert. Damit wird gezeigt, wie eine Notation, die bezüglich der Spezifikationsmächtigkeit und der Flexibilität der Typisierung über existierende typisierte objektorientierte Programmier- und Spezifikationssprachen hinausgeht, formal definiert werden kann. Die Flexibilität beruht insbesondere auf der Unterscheidung von Objekttypen und Klassen. Das zentrale methodische Konzept ist die Klassenverfeinerung. Sie erlaubt es, abstrakte, spezifizierende Klassen durch konkretere, implementierungsnähere zu ersetzen. Es wird gezeigt, daß Klassenverfeinerung durch die aus dem Verfeinerungskalkül bekannte Technik der Datenverfeinerung nachgewiesen werden kann. Für die Verfeinerung von inkrementell modifizierten Klassen werden spezielle, vereinfachte Beweisregeln aufgestellt. Das Herausfaktorisieren von Gemeinsamkeiten von Klassen wird durch zwei neuartige Operatoren, Klassenschnitt und Klassenvereinigung, unterstützt.

@misc{Sekerinski93RefinementAlgebraOOP,
	address = {London},
	title = {Refinement {Algebra} for {Object}-{Oriented} {Programming}},
	language = {(extended abstract)},
	author = {Sekerinski, E.},
	month = dec,
	year = {1993},
}

@book{CasaisEtAl93FormalObjectOrientedDevelopment,
	series = {{FZI} {Bericht}},
	title = {The {Process} of {Formal} {Object}-{Oriented} {Software} {Development}},
	publisher = {Forschungszentrum Informatik Karlsruhe},
	editor = {Casais, Eduardo and Lewerentz, Claus and Rüping, Andreas and Sekerinski, Emil and Weber, Franz},
	month = mar,
	year = {1993},
}

@techreport{Sekerinski93BehaviouralObjectTypes,
	type = {{FZI} {Bericht}},
	title = {A {Behavioural} {View} of {Object} {Types}},
	number = {7/93},
	institution = {Forschungszentrum Informatik},
	author = {Sekerinski, Emil},
	month = mar,
	year = {1993},
}

@inproceedings{Sekerinski93PredicativeProgramming,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {A {Calculus} for {Predicative} {Programming}},
	volume = {669},
	doi = {10.1007/3-540-56625-2_20},
	abstract = {A calculus for developing programs from specifications written as predicates that describe the relationship between the initial and final state is proposed. Such specifications are well known from the specification language Z. All elements of a simple sequential programming notation are defined in terms of predicates. Hence programs form a subset of specifications. In particular, sequential composition is defined by ‘demonic composition’, non-deterministic choice by ‘demonic disjunction’, and iteration by fixed points. Laws are derived which allow proving equivalence and refinement of specifications and programs by a series of steps. The weakest precondition calculus is also included. The approach is compared to the predicative programming approach of E. Hehner and to other refinement calculi.},
	booktitle = {Mathematics of {Program} {Construction}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Bird, R. S. and Morgan, C. C. and Woodcock, J. C. P.},
	month = feb,
	year = {1993},
	keywords = {ISBN 3-540-56625-2},
	pages = {302--321},
}

A calculus for developing programs from specifications written as predicates that describe the relationship between the initial and final state is proposed. Such specifications are well known from the specification language Z. All elements of a simple sequential programming notation are defined in terms of predicates. Hence programs form a subset of specifications. In particular, sequential composition is defined by ‘demonic composition’, non-deterministic choice by ‘demonic disjunction’, and iteration by fixed points. Laws are derived which allow proving equivalence and refinement of specifications and programs by a series of steps. The weakest precondition calculus is also included. The approach is compared to the predicative programming approach of E. Hehner and to other refinement calculi.

@book{LewerentzEtAl92Spezifikationsmethoden,
	series = {{FZI} {Bericht}},
	title = {Objektorientierte {Spezifikationsmethoden}},
	number = {29},
	publisher = {Forschungszentrum Informatik},
	editor = {Lewerentz, C. and Rüping, A. and Sekerinski, E. and Weber, F.},
	month = apr,
	year = {1992},
	note = {Pages: 100},
}

@book{NeumannEtAlSoftwareWiederverwendung,
	series = {{FZI} {Bericht}},
	title = {Software-{Wiederverwendung}},
	number = {27},
	publisher = {Forschungszentrum Informatik},
	editor = {Neumann, D. and Sekerinski, E. and Tick, J. and Weber, F.},
	month = nov,
	year = {1991},
	note = {Pages: 65},
}

@book{KienhoferRehmSekerinski91Softwareproduktionsumgebungen,
	series = {{FZI} {Bericht}},
	title = {Softwareproduktionsumgebungen},
	number = {22},
	publisher = {Forschungszentrum Informatik},
	editor = {Kienhöfer, J. and Rehm, S. and Sekerinski, E.},
	month = may,
	year = {1991},
	note = {Pages: 71},
}

@techreport{UhlEtAl91OBST,
	type = {{FZI} {Publikation}},
	title = {The {Object} {Management} {System} of {Stone} – {OBST} {Release} 3.0},
	institution = {Forschungszentrum Informatik},
	author = {Uhl, J. and Theobald, D. and Schiefer, B. and Sekerinski, E. and Rehm, S. and Ranft, M.},
	month = feb,
	year = {1991},
}

@techreport{UhlEtAl90ObjectManagement,
	type = {{FZI} {Publikation}},
	title = {The {Object} {Management} of {Stone} – {System} {Design} and {Implementation}},
	institution = {Forschungszentrum Informatik},
	author = {Uhl, J. and Schiefer, B. and Sekerinski, E.},
	month = oct,
	year = {1990},
}

@book{UhlSekerinski90FormaleSoftwareentwicklung,
	series = {{FZI} {Bericht}},
	title = {Formale {Methoden} der {Softwareentwicklung}},
	number = {18},
	publisher = {Forschungszentrum Informatik},
	editor = {Uhl, J. and Sekerinski, E.},
	month = jun,
	year = {1990},
}

@phdthesis{Sekerinski89,
	type = {Diplomarbeit},
	title = {Entwicklung eines korrekten {Assemblierers}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski89.pdf},
	abstract = {In dieser Arbeit wird ein Assemblierer für den MC68020 Prozessor entwickelt und gegenüber einer formalen Spezifikation als korrekt bewiesen. Die Spezifikation ist in Prädikatenlogik gegeben, und die angewandte Beweismethode ist ein auf Prädikatenlogik aufgesetzter Kalkül. Die Implementierung ist in Modula-2 geschrieben und hat, neben ihrer Korrektheit, die Vorzüge, extrem kompakt und effizient zu sein.},
	school = {Universität Karlsruhe},
	author = {Sekerinski, Emil},
	year = {1989},
}

In dieser Arbeit wird ein Assemblierer für den MC68020 Prozessor entwickelt und gegenüber einer formalen Spezifikation als korrekt bewiesen. Die Spezifikation ist in Prädikatenlogik gegeben, und die angewandte Beweismethode ist ein auf Prädikatenlogik aufgesetzter Kalkül. Die Implementierung ist in Modula-2 geschrieben und hat, neben ihrer Korrektheit, die Vorzüge, extrem kompakt und effizient zu sein.