var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https%3A%2F%2Fwww.cas.mcmaster.ca%2F~emil%2Fpublications.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https%3A%2F%2Fwww.cas.mcmaster.ca%2F~emil%2Fpublications.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https%3A%2F%2Fwww.cas.mcmaster.ca%2F~emil%2Fpublications.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
    2. \n
  2. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
    3. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2022\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Interactive Notebooks on Software Design.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n of Open LibraryeCampusOntario, June 2022.\n \n\n\n\n
\n\n\n\n \n \n \"InteractivePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{Sekerinski22SoftwareDesign,\n\tseries = {Open {Library}},\n\ttitle = {Interactive {Notebooks} on {Software} {Design}},\n\turl = {https://vlslibrary.ecampusontario.ca/item-details/#/5772cd52-86a4-4794-977c-13a2257a6e6d},\n\tabstract = {This is a collection of interactive Jupyter notebooks for teaching software design and, more specifically, concurrent system design on an upper undergraduate level.\n(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.\n(2) The notebooks use an algorithmic notation for explaining concepts and use Python, Java, and Go for programming.\n(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.\n(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.\nFor 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.},\n\tnumber = {MCMA-990/ID618},\n\tpublisher = {eCampusOntario},\n\tauthor = {Sekerinski, Emil},\n\tmonth = jun,\n\tyear = {2022},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n New Concurrent Order Maintenance Data Structure.\n \n \n \n\n\n \n Guo, B.; and Sekerinski, E.\n\n\n \n\n\n\n August 2022.\n Pages: 11\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{GuoSekerinski22ConcurrentOrderMaintenancePreprint,\n\ttitle = {New {Concurrent} {Order} {Maintenance} {Data} {Structure}},\n\tdoi = {10.48550/arXiv.2208.07800},\n\tabstract = {The Order-Maintenance (OM) data structure maintains a total order list of items for insertions, deletions, and comparisons.\nAs 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.\nThe 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.\nSpecifically, parallel insertions and deletions are synchronized by using locks efficiently, which achieve up to 7x and 5.6x speedups with 64 workers.\nOne 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.\nTypical 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.\nThis is why the lock-free order comparison is a breakthrough in practice.},\n\tauthor = {Guo, Bin and Sekerinski, Emil},\n\tmonth = aug,\n\tyear = {2022},\n\tnote = {Pages: 11},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n re:mote – Low-cost Software and Hardware Infrastructure for Water Quality Sensing in Indigenous Communities.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhou, T.\n\n\n \n\n\n\n October 2022.\n \n\n\n\n
\n\n\n\n \n \n \"re:motePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{SekerinskiZhou22ReMoteSlides,\n\taddress = {Hamilton, Ontario, Canada},\n\ttitle = {re:mote – {Low}-cost {Software} and {Hardware} {Infrastructure} for {Water} {Quality} {Sensing} in {Indigenous} {Communities}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhou22ReMoteSlides.pdf},\n\tauthor = {Sekerinski, Emil and Zhou, Tianyu},\n\tmonth = oct,\n\tyear = {2022},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Striving Towards Reconciliation through the Co-Creation of Water Research.\n \n \n \n \n\n\n \n Martin-Hill, D.; Gibson, C. M.; de Lannoy, C.; Gendron, D.; McQueen, D.; Looking Horse, M.; King, C.; Grewal, H.; Deen, T. A.; Makhdoom, S.; Chow-Fraser, P.; Sekerinski, E.; Selvaganapathy, P. R.; and Arain, M. A.\n\n\n \n\n\n\n In Indigenous Water and Drought Management in a Changing World, pages 28. Elsevier, 2022.\n \n\n\n\n
\n\n\n\n \n \n \"StrivingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{MartinHillEtAl22CoCreation,\n\ttitle = {Striving {Towards} {Reconciliation} through the {Co}-{Creation} of {Water} {Research}},\n\turl = {https://doi.org/10.1016/B978-0-12-824538-5.00002-9},\n\tabstract = {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.},\n\tbooktitle = {Indigenous {Water} and {Drought} {Management} in a {Changing} {World}},\n\tpublisher = {Elsevier},\n\tauthor = {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},\n\tyear = {2022},\n\tpages = {28},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Universal Design of Interactive Mathematical Notebooks on Programming (Poster Presentation).\n \n \n \n \n\n\n \n Guo, B.; Nagy, J.; and Sekerinski, E.\n\n\n \n\n\n\n March 2022.\n \n\n\n\n
\n\n\n\n \n \n \"UniversalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{GuoEtAl22UniversalDesignPoster,\n\taddress = {Providence, Rhode Island, USA},\n\ttype = {Poster},\n\ttitle = {Universal {Design} of {Interactive} {Mathematical} {Notebooks} on {Programming} ({Poster} {Presentation})},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/GuoEtAl22UniversalDesignPoster.webm},\n\tabstract = {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.},\n\tauthor = {Guo, Bin and Nagy, Jason and Sekerinski, Emil},\n\tmonth = mar,\n\tyear = {2022},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Simplified Algorithms for Order-Based Core Maintenance.\n \n \n \n\n\n \n Guo, B.; and Sekerinski, E.\n\n\n \n\n\n\n ,16. January 2022.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{GuoSekerinski22CoreMaintenancePreprint,\n\ttitle = {Simplified {Algorithms} for {Order}-{Based} {Core} {Maintenance}},\n\tdoi = {arXiv:2201.07103},\n\tabstract = {Graph analytics attract much attention from both research and\nindustry communities. Due to the linear time complexity, the 𝑘-\ncore decomposition is widely used in many real-world applications\nsuch as biology, social networks, community detection, ecology,\nand information spreading. In many such applications, the data\ngraphs continuously change over time. The changes correspond\nto edge insertion and removal. Instead of recomputing the 𝑘-core,\nwhich is time-consuming, we study how to maintain the 𝑘-core\nefficiently. That is, when inserting or deleting an edge, we need to\nidentify the affected vertices by searching for more vertices. The\nstate-of-the-art order-based method maintains an order, the so-\ncalled 𝑘-order, among all vertices, which can significantly reduce\nthe searching space. However, this order-based method is compli-\ncated for understanding and implementation, and its correctness is\nnot formally discussed. In this work, we propose a simplified order-\nbased approach by introducing the classical Order Data Structure to\nmaintain the 𝑘-order, which significantly improves the worst-case\ntime complexity for both edge insertion and removal algorithms.\nAlso, our simplified method is intuitive to understand and imple-\nment; it is easy to argue the correctness formally. Additionally,\nwe discuss a simplified batch insertion approach. The experiments\nevaluate our simplified method over 12 real and synthetic graphs\nwith billions of vertices. Compared with the existing method, our\nsimplified approach achieves high speedups up to 7.7x and 9.7x for\nedge insertion and removal, respectively.},\n\tauthor = {Guo, Bin and Sekerinski, Emil},\n\tmonth = jan,\n\tyear = {2022},\n\tpages = {16},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Efficient parallel graph trimming by arc-consistency.\n \n \n \n \n\n\n \n Guo, B.; and Sekerinski, E.\n\n\n \n\n\n\n The Journal of Supercomputing,1–45. April 2022.\n \n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{GuoSekerinski22ParallelGraphTrimming,\n\ttitle = {Efficient parallel graph trimming by arc-consistency},\n\tcopyright = {2022 The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature},\n\tissn = {1573-0484},\n\turl = {https://link.springer.com/article/10.1007/s11227-022-04457-9},\n\tdoi = {10.1007/s11227-022-04457-9},\n\tabstract = {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.},\n\tlanguage = {en},\n\turldate = {2022-04-18},\n\tjournal = {The Journal of Supercomputing},\n\tauthor = {Guo, Bin and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2022},\n\tpages = {1--45},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Universal Design of Interactive Mathematical Notebooks on Programming (Extended Abstract).\n \n \n \n\n\n \n Guo, B.; Nagy, J.; and Sekerinski\n\n\n \n\n\n\n In Proceedings of the 53rd ACM Technical Symposium on Computer Science Education, pages 1, Providence, Rhode Island, USA, March 2022. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{GuoEtAl22UniversalDesignAbstract,\n\taddress = {Providence, Rhode Island, USA},\n\ttitle = {Universal {Design} of {Interactive} {Mathematical} {Notebooks} on {Programming} ({Extended} {Abstract})},\n\tdoi = {10.1145/3478432.3499102},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 53rd {ACM} {Technical} {Symposium} on {Computer} {Science} {Education}},\n\tauthor = {Guo, Bin and Nagy, Jason and Sekerinski},\n\tmonth = mar,\n\tyear = {2022},\n\tpages = {1},\n}\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Efficient parallel graph trimming by arc-consistency.\n \n \n \n \n\n\n \n Guo, B.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 2021.\n Pages: 1–42\n\n\n\n
\n\n\n\n \n \n \"EfficientPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{GuoSekerinski21ParallelGraphTrimmingPreprint,\n\ttype = {Preprint},\n\ttitle = {Efficient parallel graph trimming by arc-consistency},\n\turl = {https://arxiv.org/pdf/2107.12720.pdf},\n\tabstract = {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.\nIn 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.},\n\tauthor = {Guo, Bin and Sekerinski, Emil},\n\tyear = {2021},\n\tnote = {Pages: 1–42},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Real-time prediction of river chloride concentration using ensemble learning.\n \n \n \n\n\n \n Zhang, Q.; Li, Z.; Zhu, L.; Zhang, F.; Sekerinski, E.; Han, J.; and Zhou, Y.\n\n\n \n\n\n\n Environmental Pollution, 291: 118116. 2021.\n Publisher: Elsevier\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{ZhangEtAl21EnsembleLearning,\n\ttitle = {Real-time prediction of river chloride concentration using ensemble learning},\n\tvolume = {291},\n\tdoi = {10.1016/j.envpol.2021.118116},\n\tabstract = {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.},\n\tjournal = {Environmental Pollution},\n\tauthor = {Zhang, Qianqian and Li, Zhong and Zhu, Lu and Zhang, Fei and Sekerinski, Emil and Han, Jing-Cheng and Zhou, Yang},\n\tyear = {2021},\n\tnote = {Publisher: Elsevier},\n\tpages = {118116},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Striffs: Architectural component diagrams for code reviews.\n \n \n \n \n\n\n \n Fadhel, M.; and Sekerinski, E.\n\n\n \n\n\n\n In 2021 International Conference on Code Quality (ICCQ), pages 69–78, 2021. IEEE\n \n\n\n\n
\n\n\n\n \n \n \"Striffs:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{FadhelSekerinski21Striffs,\n\ttitle = {Striffs: {Architectural} component diagrams for code reviews},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/FadhelSekerinski21StriffsPreview.pdf},\n\tdoi = {10.1109/ICCQ51190.2021.9392939},\n\tabstract = {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.},\n\tbooktitle = {2021 {International} {Conference} on {Code} {Quality} ({ICCQ})},\n\tpublisher = {IEEE},\n\tauthor = {Fadhel, Muntazir and Sekerinski, Emil},\n\tyear = {2021},\n\tpages = {69--78},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Universal Design of Interactive Notebooks on Programming.\n \n \n \n \n\n\n \n Guo, B.; Nagy, J.; and Sekerinski, E.\n\n\n \n\n\n\n December 2021.\n \n\n\n\n
\n\n\n\n \n \n \"UniversalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{GuoNagySekerinski21UniversalDesign,\n\taddress = {Hamilton, Ontario, Canada},\n\ttype = {Poster},\n\ttitle = {Universal {Design} of {Interactive} {Notebooks} on {Programming}},\n\turl = {https://mi.mcmaster.ca/innovations-in-education-conference/},\n\tabstract = {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.\nThe 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.},\n\tauthor = {Guo, Bin and Nagy, Jason and Sekerinski, Emil},\n\tmonth = dec,\n\tyear = {2021},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Extending the re:mote system for water quality measurements and turtle tracking using mobile devices and Bluetooth-enabled sensors.\n \n \n \n \n\n\n \n Sekerinski, E.; Pandya, D.; Nayeem, W.; and Srivasanthakumar, V.\n\n\n \n\n\n\n May 2021.\n \n\n\n\n
\n\n\n\n \n \n \"ExtendingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{SekerinskiEtAl21ExtendingReMote,\n\ttype = {Poster},\n\ttitle = {Extending the re:mote system for water quality measurements and turtle tracking using mobile devices and {Bluetooth}-enabled sensors},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiEtAl21ExtendingReMote.pdf},\n\tauthor = {Sekerinski, Emil and Pandya, Dhrumil and Nayeem, Waseef and Srivasanthakumar, Varshan},\n\tmonth = may,\n\tyear = {2021},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I.\n \n \n \n \n\n\n \n Sekerinski, E.; Moreira, N.; Oliveira, J. N.; Ratiu, D.; Guidotti, R.; Farrell, M.; Luckcuck, M.; Marmsoler, D.; Campos, J.; Astarte, T.; Gonnord, L.; Cerone, A.; Couto, L.; Dongol, B.; Kutrib, M.; Monteiro, P.; and Delmas, D.,\n editors.\n \n\n\n \n\n\n\n Volume 12232 of Lecture Notes in Computer ScienceSpringer, 2020.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{SekerinskiEtAl20FMWS1,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Formal {Methods}. {FM} 2019 {International} {Workshops} - {Porto}, {Portugal}, {October} 7-11, 2019, {Revised} {Selected} {Papers}, {Part} {I}},\n\tvolume = {12232},\n\tisbn = {978-3-030-54993-0},\n\turl = {https://doi.org/10.1007/978-3-030-54994-7},\n\tpublisher = {Springer},\n\teditor = {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},\n\tyear = {2020},\n\tdoi = {10.1007/978-3-030-54994-7},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II.\n \n \n \n \n\n\n \n Sekerinski, E.; Moreira, N.; Oliveira, J. N.; Ratiu, D.; Guidotti, R.; Farrell, M.; Luckcuck, M.; Marmsoler, D.; Campos, J.; Astarte, T.; Gonnord, L.; Cerone, A.; Couto, L.; Dongol, B.; Kutrib, M.; Monteiro, P.; and Delmas, D.,\n editors.\n \n\n\n \n\n\n\n Volume 12233 of Lecture Notes in Computer ScienceSpringer, 2020.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{SekerinskiEtAl20FMWS2,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Formal {Methods}. {FM} 2019 {International} {Workshops} - {Porto}, {Portugal}, {October} 7-11, 2019, {Revised} {Selected} {Papers}, {Part} {II}},\n\tvolume = {12233},\n\tisbn = {978-3-030-54996-1},\n\turl = {https://doi.org/10.1007/978-3-030-54997-8},\n\tpublisher = {Springer},\n\teditor = {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},\n\tyear = {2020},\n\tdoi = {10.1007/978-3-030-54997-8},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Comparison of Time Series Databases for Storing Water Quality Data.\n \n \n \n \n\n\n \n Fadhel, M.; Sekerinski, E.; and Yao, S.\n\n\n \n\n\n\n In Auer, M.; and Tsiatsos, T., editor(s), Mobile Technologies and Applications for the Internet of Things, IMCL 2018, volume 909, of Advances in Intelligent Systems and Computing, pages 302–313, April 2019. Springer\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{FadhelSekerinskiYao18TimeSeriesDatabases,\n\tseries = {Advances in {Intelligent} {Systems} and {Computing}},\n\ttitle = {A {Comparison} of {Time} {Series} {Databases} for {Storing} {Water} {Quality} {Data}},\n\tvolume = {909},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/FadhelSekerinskiYao18TimeSeriesDatabasesSlides.pdf},\n\tdoi = {10.1007/978-3-030-11434-3_33},\n\tabstract = {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.},\n\tbooktitle = {Mobile {Technologies} and {Applications} for the {Internet} of {Things}, {IMCL} 2018},\n\tpublisher = {Springer},\n\tauthor = {Fadhel, Muntazir and Sekerinski, Emil and Yao, Shucai},\n\teditor = {Auer, M. and Tsiatsos, T.},\n\tmonth = apr,\n\tyear = {2019},\n\tpages = {302--313},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automated Detection of Anomalies in High Frequency Water Quality Sensor Data using Machine Learning.\n \n \n \n \n\n\n \n Wang, X.; Sekerinski, E.; and Copp, J.\n\n\n \n\n\n\n In 48th Annual WEAO Technical Symposium & OPCEA Exhibition, pages 16, Toronto, Canada, April 2019. Water Environment Association of Ontario\n \n\n\n\n
\n\n\n\n \n \n \"AutomatedPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{WangSekerinskiCopp19AnomalyDetection,\n\taddress = {Toronto, Canada},\n\ttitle = {Automated {Detection} of {Anomalies} in {High} {Frequency} {Water} {Quality} {Sensor} {Data} using {Machine} {Learning}},\n\tshorttitle = {{WangSekerinskiCopp19AnomalyDetection}.pdf},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/WangSekerinskiCopp19AnomalyDetection.pdf},\n\tabstract = {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.},\n\tbooktitle = {48th {Annual} {WEAO} {Technical} {Symposium} \\& {OPCEA} {Exhibition}},\n\tpublisher = {Water Environment Association of Ontario},\n\tauthor = {Wang, Xi and Sekerinski, Emil and Copp, John},\n\tmonth = apr,\n\tyear = {2019},\n\tpages = {16},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n When Grab Samples Just Won’t do: High-Quality High-Frequency Water Quality Monitoring.\n \n \n \n \n\n\n \n Copp, J. B.; Pooni, P.; Lai, W.; Wang, X.; Viveros, R.; and Sekerinski, E.\n\n\n \n\n\n\n In 48th Annual WEAO Technical Symposium & OPCEA Exhibition, pages 4, Toronto, Canada, April 2019. Water Environment Association of Ontario\n \n\n\n\n
\n\n\n\n \n \n \"WhenPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{CoppEtAl19GrabSamples,\n\taddress = {Toronto, Canada},\n\ttitle = {When {Grab} {Samples} {Just} {Won}’t do: {High}-{Quality} {High}-{Frequency} {Water} {Quality} {Monitoring}},\n\tshorttitle = {{CoppEtAl19GrabSamples}.pdf, {CoppEtAl19GrabSamplesSlides}.pdf},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/CoppEtAl19GrabSamplesSlides.pdf},\n\tabstract = {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.},\n\tbooktitle = {48th {Annual} {WEAO} {Technical} {Symposium} \\& {OPCEA} {Exhibition}},\n\tpublisher = {Water Environment Association of Ontario},\n\tauthor = {Copp, John B. and Pooni, Prabhbir and Lai, Winfield and Wang, Xi and Viveros, Roman and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2019},\n\tpages = {4},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n re:mote – Low-cost Software and Hardware Infrastructure for Water Quality Sensing in Indigenous Communities.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n May 2019.\n \n\n\n\n
\n\n\n\n \n \n \"re:motePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{SekerinskiEtAl19ReMotePoster,\n\taddress = {Saskatoon, SK, Canada},\n\ttype = {Poster},\n\ttitle = {re:mote – {Low}-cost {Software} and {Hardware} {Infrastructure} for {Water} {Quality} {Sensing} in {Indigenous} {Communities}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiEtAl19ReMotePoster.pdf},\n\tabstract = {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.},\n\tauthor = {Sekerinski, Emil},\n\tmonth = may,\n\tyear = {2019},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Teaching Concurrency with the Disappearing Formal Method.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Dongol, B.; Petre, L.; and Smith, G., editor(s), Formal Methods Teaching, volume 11758, of Lecture Notes in Computer Science, pages 135–149, 2019. Springer, Cham\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{sekerinskiTeachingConcurrencyDisappearing2019,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Teaching {Concurrency} with the {Disappearing} {Formal} {Method}},\n\tvolume = {11758},\n\tisbn = {978-3-030-32441-4},\n\tdoi = {10.1007/978-3-030-32441-4_9},\n\tabstract = {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.},\n\tlanguage = {en},\n\tbooktitle = {Formal {Methods} {Teaching}},\n\tpublisher = {Springer, Cham},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Dongol, Brijesh and Petre, Luigia and Smith, Graeme},\n\tyear = {2019},\n\tkeywords = {Guarded commands, Non-interference, State diagrams},\n\tpages = {135--149},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An object model for dynamic mixins.\n \n \n \n\n\n \n Burton, E.; and Sekerinski, E.\n\n\n \n\n\n\n Computer Languages, Systems & Structures, 51: 90–101. January 2018.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@article{BurtonSekerinski18ObjectModelDynamicMixins,\n\ttitle = {An object model for dynamic mixins},\n\tvolume = {51},\n\tdoi = {10.1016/j.cl.2017.07.001},\n\tabstract = {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.},\n\tjournal = {Computer Languages, Systems \\& Structures},\n\tauthor = {Burton, Eden and Sekerinski, Emil},\n\tmonth = jan,\n\tyear = {2018},\n\tkeywords = {Mixins, Object models, Programming language implementations},\n\tpages = {90--101},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Notebook Format for the Holistic Design of Embedded Systems (Tool Paper).\n \n \n \n \n\n\n \n Park, S.; and Sekerinski, E.\n\n\n \n\n\n\n In Masci, P.; Monahan, R.; and Prevosto, V., editor(s), Proceedings 4th Workshop on Formal Integrated Development Environment, Oxford, England, 14 July 2018, volume 284, of Electronic Proceedings in Theoretical Computer Science, pages 85–94, November 2018. Open Publishing Association\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{parkNotebookFormatHolistic2018a,\n\tseries = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},\n\ttitle = {A {Notebook} {Format} for the {Holistic} {Design} of {Embedded} {Systems} ({Tool} {Paper})},\n\tvolume = {284},\n\turl = {http://eptcs.web.cse.unsw.edu.au/content.cgi?FIDE2018},\n\tdoi = {10.4204/EPTCS.284.7},\n\tabstract = {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.},\n\tbooktitle = {Proceedings 4th {Workshop} on {Formal} {Integrated} {Development} {Environment}, {Oxford}, {England}, 14 {July} 2018},\n\tpublisher = {Open Publishing Association},\n\tauthor = {Park, Spencer and Sekerinski, Emil},\n\teditor = {Masci, Paolo and Monahan, Rosemary and Prevosto, Virgile},\n\tmonth = nov,\n\tyear = {2018},\n\tpages = {85--94},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Programming in the Multi-Core Era.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n June 2018.\n \n\n\n\n
\n\n\n\n \n \n \"ProgrammingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{Sekerinski18MultiCoreEraSlides,\n\taddress = {Hamilton, Ontario, Canada},\n\ttype = {Talk},\n\ttitle = {Programming in the {Multi}-{Core} {Era}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski18MultiCoreEraSlides.pdf},\n\tauthor = {Sekerinski, Emil},\n\tmonth = jun,\n\tyear = {2018},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Refining Santa: An Exercise in Efficient Synchronization.\n \n \n \n \n\n\n \n Sekerinski, E.; and Yao, S.\n\n\n \n\n\n\n In Derrick, J.; Dongol, B.; and Reeves, S., editor(s), Proceedings 18th Refinement Workshop, Oxford, UK, 18th July 2018, volume 282, of Electronic Proceedings in Theoretical Computer Science, pages 68–86, October 2018. Open Publishing Association\n \n\n\n\n
\n\n\n\n \n \n \"RefiningPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{SekerinskiYao18RefiningSanta,\n\tseries = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},\n\ttitle = {Refining {Santa}: {An} {Exercise} in {Efficient} {Synchronization}},\n\tvolume = {282},\n\turl = {http://eptcs.web.cse.unsw.edu.au/content.cgi?Refine2018},\n\tdoi = {10.4204/EPTCS.282.6},\n\tabstract = {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.},\n\tbooktitle = {Proceedings 18th {Refinement} {Workshop}, {Oxford}, {UK}, 18th {July} 2018},\n\tpublisher = {Open Publishing Association},\n\tauthor = {Sekerinski, Emil and Yao, Shucai},\n\teditor = {Derrick, John and Dongol, Brijesh and Reeves, Steve},\n\tmonth = oct,\n\tyear = {2018},\n\tpages = {68--86},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Work-in-progress: modelling probabilistic timing analysis.\n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Proceedings of the Thirteenth ACM International Conference on Embedded Software 2017, EMSOFT '17, October 2017. ACM New York\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{NokovicSekerinski17ModellingProbabilisticTimingAnalysis,\n\ttitle = {Work-in-progress: modelling probabilistic timing analysis},\n\tdoi = {https://doi.org/10.1145/3125503.3125566},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the {Thirteenth} {ACM} {International} {Conference} on {Embedded} {Software} 2017, {EMSOFT} '17},\n\tpublisher = {ACM New York},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = oct,\n\tyear = {2017},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Molnos, A.; and Fabre, C., editor(s), Model-Implementation Fidelity in Cyber Physical System Design, pages 175–199, 2017. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n \n \"AnalysisPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{NokovicSekerinski17Tags,\n\ttitle = {Analysis and {Implementation} of {Embedded} {System} {Models}: {Example} of {Tags} in {Item} {Management} {Application}},\n\tisbn = {978-3-319-47307-9},\n\turl = {http://dx.doi.org/10.1007/978-3-319-47307-9_7},\n\tdoi = {10.1007/978-3-319-47307-9_7},\n\tbooktitle = {Model-{Implementation} {Fidelity} in {Cyber} {Physical} {System} {Design}},\n\tpublisher = {Springer International Publishing},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Molnos, Anca and Fabre, Christian},\n\tyear = {2017},\n\tpages = {175--199},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Object Model for a Dynamic Mixin Based Language.\n \n \n \n\n\n \n Burton, E.; and Sekerinski, E.\n\n\n \n\n\n\n In Proceedings of the 31st Annual ACM Symposium on Applied Computing, Object Oriented Programming Languages and Systems Track, of SAC'16, pages 1986–1992, Pisa, Italy, April 2016. ACM\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{burtonObjectModelDynamic2016,\n\taddress = {Pisa, Italy},\n\tseries = {{SAC}'16},\n\ttitle = {An {Object} {Model} for a {Dynamic} {Mixin} {Based} {Language}},\n\tdoi = {10.1145/2851613.2851755},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 31st {Annual} {ACM} {Symposium} on {Applied} {Computing}, {Object} {Oriented} {Programming} {Languages} and {Systems} {Track}},\n\tpublisher = {ACM},\n\tauthor = {Burton, Eden and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2016},\n\tkeywords = {mixins, object models, programming language implementations},\n\tpages = {1986--1992},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From Action Systems to Distributed Systems—The Refinement Approach.\n \n \n \n \n\n\n \n Petre, L.; and Sekerinski, E.,\n editors.\n \n\n\n \n\n\n\n Chapman and Hall/CRC, April 2016.\n \n\n\n\n
\n\n\n\n \n \n \"FromPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{PetreSekerinski16ActionToDistributed,\n\ttitle = {From {Action} {Systems} to {Distributed} {Systems}—{The} {Refinement} {Approach}},\n\turl = {https://www.crcpress.com/From-Action-Systems-to-Distributed-Systems-The-Refinement-Approach/Petre-Sekerinski/p/book/9781498701587},\n\tabstract = {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.\n\nA 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.\n\nA 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.\n\nPresenting 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.\n\nExamining 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.},\n\tpublisher = {Chapman and Hall/CRC},\n\teditor = {Petre, Luigia and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2016},\n\tdoi = {10.1201/b20053},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automatic Quantitative Analysis and Code Generator for Sensor Systems: The Example of Great Lakes Water Quality Monitoring.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Mandler, B.; Marquez-Barja, J.; Mitre Campista, M. E.; Cagáňová, D.; Chaouchi, H.; Zeadally, S.; Badra, M.; Giordano, S.; Fazio, M.; Somov, A.; and Vieriu, R., editor(s), Internet of Things. IoT Infrastructures: Second International Summit, IoT 360º, Rome, Italy, October 27-29, 2015, Revised Selected Papers, Part II, pages 313–319, 2016. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n \n \"AutomaticPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{NokovicSekerinski16GreatLakes,\n\ttitle = {Automatic {Quantitative} {Analysis} and {Code} {Generator} for {Sensor} {Systems}: {The} {Example} of {Great} {Lakes} {Water} {Quality} {Monitoring}},\n\tisbn = {978-3-319-47075-7},\n\turl = {http://dx.doi.org/10.1007/978-3-319-47075-7_35},\n\tdoi = {10.1007/978-3-319-47075-7_35},\n\tabstract = {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.},\n\tbooktitle = {Internet of {Things}. {IoT} {Infrastructures}: {Second} {International} {Summit}, {IoT} 360º, {Rome}, {Italy}, {October} 27-29, 2015, {Revised} {Selected} {Papers}, {Part} {II}},\n\tpublisher = {Springer International Publishing},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {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},\n\tyear = {2016},\n\tpages = {313--319},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Model-based WCET Analysis with Invariants.\n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Grov, G.; and Ireland, A., editor(s), Proceedings of the 15th International Workshop on Automated Verification of Critical Systems, AVoCS 2015, volume 72, of Electronic Communications of the EASST, pages 1–15, Edinburgh, United Kingdom, September 2015. European Association of Software Science and Technology\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{nokovicModelbasedWCETAnalysis2015,\n\taddress = {Edinburgh, United Kingdom},\n\tseries = {Electronic {Communications} of the {EASST}},\n\ttitle = {Model-based {WCET} {Analysis} with {Invariants}},\n\tvolume = {72},\n\tdoi = {10.14279/tuj.eceasst.72.1026.1010},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 15th {International} {Workshop} on {Automated} {Verification} of {Critical} {Systems}, {AVoCS} 2015},\n\tpublisher = {European Association of Software Science and Technology},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Grov, Gudmund and Ireland, Andrew},\n\tmonth = sep,\n\tyear = {2015},\n\tpages = {1--15},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Analysis and Implementation of Embedded System Models: Example of Tags in Item Management Application.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n March 2015.\n \n\n\n\n
\n\n\n\n \n \n \"AnalysisPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{NokovicSekerinski15TagsPresentation.pdf,\n\taddress = {Grenoble, France},\n\ttype = {Talk},\n\ttitle = {Analysis and {Implementation} of {Embedded} {System} {Models}: {Example} of {Tags} in {Item} {Management} {Application}},\n\tcopyright = {https://www.date-conference.com/date15/conference/workshop-w01},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski15TagsPresentation.pdf},\n\tabstract = {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.},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = mar,\n\tyear = {2015},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Holistic Approach in Embedded System Development.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Dubois, C.; Masci, P.; and Méry, D., editor(s), Proceedings Second International Workshop on Formal Integrated Development Environment, volume 187, of Electronic Proceedings in Theoretical Computer Science, pages 72–85, Oslo, Norway, June 2015. Open Publishing Association\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{nokovicHolisticApproachEmbedded2015,\n\taddress = {Oslo, Norway},\n\tseries = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},\n\ttitle = {A {Holistic} {Approach} in {Embedded} {System} {Development}},\n\tvolume = {187},\n\turl = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2015.6},\n\tdoi = {10.4204/EPTCS.187.6},\n\tabstract = {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.},\n\tbooktitle = {Proceedings {Second} {International} {Workshop} on {Formal} {Integrated} {Development} {Environment}},\n\tpublisher = {Open Publishing Association},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Dubois, Catherine and Masci, Paolo and Méry, Dominique},\n\tmonth = jun,\n\tyear = {2015},\n\tpages = {72--85},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Safety of Dynamic Mixin Composition.\n \n \n \n\n\n \n Burton, E.; and Sekerinski, E.\n\n\n \n\n\n\n In Proceedings of the 30th Annual ACM Symposium on Applied Computing, SAC'15, Object Oriented Programming Languages and Systems Track, pages 1992–1999, Salamanca, Spain, April 2015. ACM\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{burtonSafetyDynamicMixin2015,\n\taddress = {Salamanca, Spain},\n\ttitle = {The {Safety} of {Dynamic} {Mixin} {Composition}},\n\tdoi = {10.1145/2695664.2695938},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 30th {Annual} {ACM} {Symposium} on {Applied} {Computing}, {SAC}'15, {Object} {Oriented} {Programming} {Languages} and {Systems} {Track}},\n\tpublisher = {ACM},\n\tauthor = {Burton, Eden and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2015},\n\tpages = {1992--1999},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Generic Parallel Patterns in Lime.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n Technical Report McMaster University, Department of Computing and Software, November 2014.\n \n\n\n\n
\n\n\n\n \n \n \"GenericPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{SekerinskiZhang14PatternsInLime,\n\ttype = {{CAS} {Technical} {Report}},\n\ttitle = {Generic {Parallel} {Patterns} in {Lime}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang14PatternsInLime.pdf},\n\tabstract = {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.},\n\tinstitution = {McMaster University, Department of Computing and Software},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\tmonth = nov,\n\tyear = {2014},\n\tpages = {24},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Using Dynamic Mixins to Implement Design Patterns.\n \n \n \n\n\n \n Burton, E.; and Sekerinski, E.\n\n\n \n\n\n\n In Heesch, U. v., editor(s), Proceedings of the 19th European Conference on Pattern Languages of Programs, of EuroPLoP '14, pages 14:1–14:19, Kloster Irsee, Bavaria, Germany, July 2014. ACM\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{burtonUsingDynamicMixins2014,\n\taddress = {Kloster Irsee, Bavaria, Germany},\n\tseries = {{EuroPLoP} '14},\n\ttitle = {Using {Dynamic} {Mixins} to {Implement} {Design} {Patterns}},\n\tdoi = {10.1145/2721956.2721991},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 19th {European} {Conference} on {Pattern} {Languages} of {Programs}},\n\tpublisher = {ACM},\n\tauthor = {Burton, Eden and Sekerinski, Emil},\n\teditor = {Heesch, Uwe van},\n\tmonth = jul,\n\tyear = {2014},\n\tpages = {14:1--14:19},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Case Studies in Program Design for Heterogeneous Parallelism.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n Technical Report CAS-14-03-ES, McMaster University, Department of Computing and Software, March 2014.\n \n\n\n\n
\n\n\n\n \n \n \"CasePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{SekerinskiZhang14CaseStudiesHeterogenerousParallelism,\n\ttype = {{CAS} {Technical} {Report}},\n\ttitle = {Case {Studies} in {Program} {Design} for {Heterogeneous} {Parallelism}},\n\tcopyright = {http://www.cas.mcmaster.ca/cas/0reports/CAS-14-03-ES.pdf},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang14CaseStudiesHeterogenerousParallelism.pdf},\n\tabstract = {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.},\n\tnumber = {CAS-14-03-ES},\n\tinstitution = {McMaster University, Department of Computing and Software},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\tmonth = mar,\n\tyear = {2014},\n\tpages = {171},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verification and Code Generation for Timed Transitions in pCharts.\n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Desai, B. C., editor(s), C3S2E '14: Proceedings of the 2014 International C* Conference on Computer Science & Software Engineering, pages 3:1–3:10, Montreal, Quebec, Canada, August 2014. ACM\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{NokovicSekerinski14TimedpCharts,\n\taddress = {Montreal, Quebec, Canada},\n\ttitle = {Verification and {Code} {Generation} for {Timed} {Transitions} in {pCharts}},\n\tdoi = {10.1145/2641483.2641522},\n\tabstract = {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.},\n\tbooktitle = {{C3S2E} '14: {Proceedings} of the 2014 {International} {C}* {Conference} on {Computer} {Science} \\& {Software} {Engineering}},\n\tpublisher = {ACM},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Desai, Bipin C.},\n\tmonth = aug,\n\tyear = {2014},\n\tpages = {3:1--3:10},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Integrated Formal Methods–11th International Conference, IFM 2014, Bertinoro, Italy.\n \n \n \n\n\n \n Albert, E.; and Sekerinski, E.,\n editors.\n \n\n\n \n\n\n\n Volume 8739 of Lecture Notes in Computer ScienceSpringer, September 2014.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{albertIntegratedFormalMethods2014,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Integrated {Formal} {Methods}–11th {International} {Conference}, {IFM} 2014, {Bertinoro}, {Italy}},\n\tvolume = {8739},\n\tpublisher = {Springer},\n\teditor = {Albert, Elvira and Sekerinski, Emil},\n\tmonth = sep,\n\tyear = {2014},\n\tdoi = {10.1007/978-3-319-10181-1},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Comparison of Scalable Multi-Threaded Stack Mechanisms.\n \n \n \n \n\n\n \n Moore-Oliva, J.; Sekerinski, E.; and Yao, S.\n\n\n \n\n\n\n Technical Report CAS-14-07-ES, McMaster University, Department of Computing and Software, April 2014.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{MooreOlivaSekerinskiYao14MultiThreadedStack,\n\ttype = {{CAS} {Technical} {Report}},\n\ttitle = {A {Comparison} of {Scalable} {Multi}-{Threaded} {Stack} {Mechanisms}},\n\tcopyright = {http://www.cas.mcmaster.ca/cas/0reports/CAS-14-07-ES.pdf},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/MooreOlivaSekerinskiYao14MultiThreadedStack.pdf},\n\tabstract = {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.\nIn 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.},\n\tnumber = {CAS-14-07-ES},\n\tinstitution = {McMaster University, Department of Computing and Software},\n\tauthor = {Moore-Oliva, Joshua and Sekerinski, Emil and Yao, Shucai},\n\tmonth = apr,\n\tyear = {2014},\n\tpages = {10},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Modelling Power Consumption and Transmission Reliability of Motes.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n July 2014.\n \n\n\n\n
\n\n\n\n \n \n \"ModellingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{NokovicSekerinski14ModellingMotes,\n\ttype = {Poster},\n\ttitle = {Modelling {Power} {Consumption} and {Transmission} {Reliability} of {Motes}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski14ModellingMotes.pdf},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = jul,\n\tyear = {2014},\n\tannote = {Poster Presentation, Challenges in Water Monitoring, McMaster University},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Finitary Fairness in Action Systems.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n In Liu, Z.; Woodcock, J.; and Zhu, H., editor(s), Theoretical Aspects of Computing–ICTAC 2013, 10th International Colloquium, volume 8049, of Lecture Notes in Computer Science, pages 319–336, Shanghai, China, September 2013. Springer Berlin Heidelberg\n \n\n\n\n
\n\n\n\n \n \n \"FinitaryPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{sekerinskiFinitaryFairnessAction2013,\n\taddress = {Shanghai, China},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Finitary {Fairness} in {Action} {Systems}},\n\tvolume = {8049},\n\tisbn = {978-3-642-39717-2},\n\turl = {http://dx.doi.org/10.1007/978-3-642-39718-9_19},\n\tdoi = {10.1007/978-3-642-39718-9_19},\n\tabstract = {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.},\n\tbooktitle = {Theoretical {Aspects} of {Computing}–{ICTAC} 2013, 10th {International} {Colloquium}},\n\tpublisher = {Springer Berlin Heidelberg},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\teditor = {Liu, Zhiming and Woodcock, Jim and Zhu, Huibiao},\n\tmonth = sep,\n\tyear = {2013},\n\tkeywords = {Event-B, Finitary Fairness, Modelling, Stepwise Refinement, Termination},\n\tpages = {319--336},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Correctness of intrusive data structures using mixins.\n \n \n \n \n\n\n \n Burton, E.; and Sekerinski, E.\n\n\n \n\n\n\n In Proceedings of the 16th International ACM Sigsoft Symposium on Component-Based Software Engineering, of CBSE '13, pages 53–58, Vancouver, British Columbia, Canada, June 2013. ACM\n \n\n\n\n
\n\n\n\n \n \n \"CorrectnessPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{burtonCorrectnessIntrusiveData2013,\n\taddress = {Vancouver, British Columbia, Canada},\n\tseries = {{CBSE} '13},\n\ttitle = {Correctness of intrusive data structures using mixins},\n\tisbn = {978-1-4503-2122-8},\n\turl = {http://doi.acm.org/10.1145/2465449.2465466},\n\tdoi = {10.1145/2465449.2465466},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 16th {International} {ACM} {Sigsoft} {Symposium} on {Component}-{Based} {Software} {Engineering}},\n\tpublisher = {ACM},\n\tauthor = {Burton, Eden and Sekerinski, Emil},\n\tmonth = jun,\n\tyear = {2013},\n\tkeywords = {mixins, refinements},\n\tpages = {53--58},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On a New Notion of Partial Refinement.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n In Derrick, J.; Boiten, E.; and Reeves, S., editor(s), Proceedings of the 16th International Refinement Workshop, volume 115, of Electronic Proceedings in Theoretical Computer Science, pages 1 – 14, Turku, Finland, May 2013. \n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{SekerinskiZhang13PartialRefinement,\n\taddress = {Turku, Finland},\n\tseries = {Electronic {Proceedings} in {Theoretical} {Computer} {Science}},\n\ttitle = {On a {New} {Notion} of {Partial} {Refinement}},\n\tvolume = {115},\n\turl = {http://arxiv.org/abs/1305.6110v1},\n\tdoi = {10.4204/EPTCS.115.1},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 16th {International} {Refinement} {Workshop}},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\teditor = {Derrick, John and Boiten, Eerke and Reeves, Steve},\n\tmonth = may,\n\tyear = {2013},\n\tpages = {1 -- 14},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n pState: A Probabilistic Statecharts Translator.\n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n In Stojanović, R.; Jóźwiak, L.; and Lutovac, B., editor(s), Embedded Computing (MECO), 2nd Mediterranean Conference on, pages 29–32, Budva, Montenegro, June 2013. IEEE Press\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{nokovicPStateProbabilisticStatecharts2013,\n\taddress = {Budva, Montenegro},\n\ttitle = {{pState}: {A} {Probabilistic} {Statecharts} {Translator}},\n\tdoi = {10.1109/MECO.2013.6601339},\n\tabstract = {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.},\n\tbooktitle = {Embedded {Computing} ({MECO}), 2nd {Mediterranean} {Conference} on},\n\tpublisher = {IEEE Press},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\teditor = {Stojanović, Radovan and Jóźwiak, Lech and Lutovac, Budimir},\n\tmonth = jun,\n\tyear = {2013},\n\tkeywords = {verification, Computational modeling, invariants, model-checking, quantitative properties, statecharts},\n\tpages = {29--32},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Verification Rules for Exception Handling in Eiffel.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n In Gheyi, R.; and Naumann, D., editor(s), Formal Methods: Foundations and Applications, volume 7498, of Lecture Notes in Computer Science, pages 179–193, Natal, Brazil, September 2012. Springer\n \n\n\n\n
\n\n\n\n \n \n \"VerificationPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{sekerinskiVerificationRulesException2012,\n\taddress = {Natal, Brazil},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Verification {Rules} for {Exception} {Handling} in {Eiffel}},\n\tvolume = {7498},\n\tisbn = {978-3-642-33295-1},\n\turl = {http://dx.doi.org/10.1007/978-3-642-33296-8_14},\n\tabstract = {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.},\n\tbooktitle = {Formal {Methods}: {Foundations} and {Applications}},\n\tpublisher = {Springer},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\teditor = {Gheyi, Rohit and Naumann, David},\n\tmonth = sep,\n\tyear = {2012},\n\tpages = {179--193},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Tutorial on Exception Handling.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n February 2012.\n \n\n\n\n
\n\n\n\n \n \n \"TutorialPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@misc{Sekerinski12TutorialExceptionHandling,\n\taddress = {Abo Akademi, Turku, Finland},\n\ttype = {Tutorial},\n\ttitle = {Tutorial on {Exception} {Handling}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski12TutorialExceptionHandling.pdf},\n\tauthor = {Sekerinski, Emil},\n\tmonth = feb,\n\tyear = {2012},\n\tannote = {Presented at NODES Winter School and Seminar, 1 - 3 February 2012 Turku, Finland},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Pascal0 Compiler.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zingaro, D.\n\n\n \n\n\n\n Technical Report McMaster University, Department of Computing and Software, January 2011.\n \n\n\n\n
\n\n\n\n \n \n \"Pascal0Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{SekerinskiZingaro11Pascal0,\n\ttype = {{CAS} {Technical} {Report}},\n\ttitle = {Pascal0 {Compiler}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZingaro11Pascal0.pdf},\n\tabstract = {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.},\n\tinstitution = {McMaster University, Department of Computing and Software},\n\tauthor = {Sekerinski, Emil and Zingaro, Daniel},\n\tmonth = jan,\n\tyear = {2011},\n\tpages = {48},\n\tannote = {Revised Version},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Power Modelling and Power Analysis of Electronic Tag: A Case Study Using Probabilistic Model Checking.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 63, McMaster University, April 2011.\n \n\n\n\n
\n\n\n\n \n \n \"PowerPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{NokovicSekerinski11PowerModelling,\n\ttype = {{SQRL} {Report}},\n\ttitle = {Power {Modelling} and {Power} {Analysis} of {Electronic} {Tag}: {A} {Case} {Study} {Using} {Probabilistic} {Model} {Checking}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski11PowerModelling.pdf},\n\tabstract = {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.},\n\tnumber = {63},\n\tinstitution = {McMaster University},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {2011},\n\tpages = {14},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Normal Form for Multi-Exit Statements.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n Technical Report 2011.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{SekerinskiZhang11NormalFormMultiExit,\n\ttype = {{CAS} {Technical} {Report}},\n\ttitle = {A {Normal} {Form} for {Multi}-{Exit} {Statements}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang11NormalFormMultiExit.pdf},\n\tabstract = {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.},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\tyear = {2011},\n\tpages = {16},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Exceptions for Dependability.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Petre, L.; Sere, K.; and Troubitsyna, E., editor(s), Dependability and Computer Engineering: Concepts for Software-Intensive Systems—a Handbook on Dependability Research, pages 11–35. IGI Global, July 2011.\n \n\n\n\n
\n\n\n\n \n \n \"ExceptionsPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{Sekerinski11ExceptionsDependability,\n\ttitle = {Exceptions for {Dependability}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski11ExceptionsDependability.pdf},\n\tabstract = {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.},\n\tbooktitle = {Dependability and {Computer} {Engineering}: {Concepts} for {Software}-{Intensive} {Systems}—a {Handbook} on {Dependability} {Research}},\n\tpublisher = {IGI Global},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Petre, Luigia and Sere, Kaisa and Troubitsyna, Elena},\n\tmonth = jul,\n\tyear = {2011},\n\tdoi = {10.4018/978-1-60960-747-0},\n\tpages = {11--35},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A New Notion of Partial Correctness for Exception Handling.\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n In Bonakdarpour, B.; and Maibaum, T., editor(s), Proceedings of the 2nd International Workshop on Logical Aspects of Fault-Tolerance, pages 116–132, June 2011. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{sekerinskiNewNotionPartial2011,\n\ttitle = {A {New} {Notion} of {Partial} {Correctness} for {Exception} {Handling}},\n\tcopyright = {https://ece.uwaterloo.ca/ bbonakda/LAFT11/papers/proc.pdf},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/BonakdarpourMaibaum11LAFT.pdf},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 2nd {International} {Workshop} on {Logical} {Aspects} of {Fault}-{Tolerance}},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\teditor = {Bonakdarpour, Borzoo and Maibaum, Tom},\n\tmonth = jun,\n\tyear = {2011},\n\tpages = {116--132},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Analysis of Interrogator-tag Communication Protocols.\n \n \n \n \n\n\n \n Nokovic, B.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 60, McMaster University, Hamilton, Ontario, Canada, December 2010.\n \n\n\n\n
\n\n\n\n \n \n \"AnalysisPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{NokovicSekerinski10Interrogator,\n\taddress = {Hamilton, Ontario, Canada},\n\ttype = {{SQRL} {Report}},\n\ttitle = {Analysis of {Interrogator}-tag {Communication} {Protocols}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/NokovicSekerinski10Interrogator.pdf},\n\tabstract = {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.},\n\tnumber = {60},\n\tinstitution = {McMaster University},\n\tauthor = {Nokovic, Bojan and Sekerinski, Emil},\n\tmonth = dec,\n\tyear = {2010},\n\tpages = {20},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finitary Fairness in Event-B (Extended Abstract).\n \n \n \n \n\n\n \n Sekerinski, E.; and Zhang, T.\n\n\n \n\n\n\n In Abrial, J.; Butler, M.; Joshi, R.; Troubitsyna, E.; and Woodcock, J. C. P., editor(s), Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems, of 5 pages, Dagstuhl, Germany, January 2010. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany\n \n\n\n\n
\n\n\n\n \n \n \"FinitaryPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{sekerinskiFinitaryFairnessEventB2010,\n\taddress = {Dagstuhl, Germany},\n\tseries = {5 pages},\n\ttitle = {Finitary {Fairness} in {Event}-{B} ({Extended} {Abstract})},\n\tcopyright = {http://drops.dagstuhl.de/portals/09381/},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiZhang10FinitaryFairness.pdf},\n\tbooktitle = {Dagstuhl {Seminar} on {Refinement} {Based} {Methods} for the {Construction} of {Dependable} {Systems}},\n\tpublisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\teditor = {Abrial, Jean-Raymond and Butler, Michael and Joshi, Rajeev and Troubitsyna, Elena and Woodcock, Jim C. P.},\n\tmonth = jan,\n\tyear = {2010},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Proceedings of Formal Methods 2009 Doctoral Symposium.\n \n \n \n \n\n\n \n Mousavi, M.; and Sekerinski, E.,\n editors.\n \n\n\n \n\n\n\n TU Eindhoven, November 2009.\n \n\n\n\n
\n\n\n\n \n \n \"ProceedingsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{MousaviSekerinski09FMDS,\n\ttitle = {Proceedings of {Formal} {Methods} 2009 {Doctoral} {Symposium}},\n\tcopyright = {http://www.win.tue.nl/fm2009/DoctoralSymposium/fm09ds.pdf},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/MousaviSekerinski09FMDS.pdf},\n\tpublisher = {TU Eindhoven},\n\teditor = {Mousavi, MohammadReza and Sekerinski, Emil},\n\tmonth = nov,\n\tyear = {2009},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Design Verification with State Invariants.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Lano, K., editor(s), UML 2 Semantics and Applications, pages 317–347. John Wiley & Sons, October 2009.\n URL: https://onlinelibrary.wiley.com/doi/10.1002/9780470522622.ch13\n\n\n\n
\n\n\n\n \n \n \"DesignPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 8 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@incollection{Sekerinski09StateInvariants,\n\ttitle = {Design {Verification} with {State} {Invariants}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski09StateInvariants.pdf},\n\tabstract = {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},\n\tbooktitle = {{UML} 2 {Semantics} and {Applications}},\n\tpublisher = {John Wiley \\& Sons},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Lano, Kevin},\n\tmonth = oct,\n\tyear = {2009},\n\tdoi = {10.1002/9780470522622.ch13},\n\tnote = {URL: https://onlinelibrary.wiley.com/doi/10.1002/9780470522622.ch13},\n\tkeywords = {accumulated invariants and targeted verification condition generation, design verification with state invariants, self-transition and interlevel transition},\n\tpages = {317--347},\n\tannote = {Print ISBN: 9780470409084 Online ISBN: 9780470522622 DOI: 10.1002/9780470522622.ch13 US: http://dx.doi.org/10.1002/9780470522622.ch13 },\n}\n\n
\n
\n\n\n
\n 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\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Teaching the Unifying Mathematics of Software Design.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Brouwer, R.; Cukierman, D.; and Tsiknis, G., editor(s), Proceedings of the 14th Western Canadian Conference on Computing Education, of WCCCE '09, pages 109–115, Burnaby, British Columbia, Canada, May 2009. ACM\n \n\n\n\n
\n\n\n\n \n \n \"TeachingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski09UnifyingMathematicsSoftwareDesignPreprint,\n\taddress = {Burnaby, British Columbia, Canada},\n\tseries = {{WCCCE} '09},\n\ttitle = {Teaching the {Unifying} {Mathematics} of {Software} {Design}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski09UnifyingMathematicsSoftwareDesignPreprint.pdf},\n\tdoi = {10.1145/1536274.1536307},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 14th {Western} {Canadian} {Conference} on {Computing} {Education}},\n\tpublisher = {ACM},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Brouwer, R. and Cukierman, D. and Tsiknis, G.},\n\tmonth = may,\n\tyear = {2009},\n\tpages = {109--115},\n\tannote = { isbn = 978-1-60558-415-7 doi = http://doi.acm.org/10.1145/1536274.1536307 address = New York, NY, USA},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Experimental Implementation of Action-Based Concurrency.\n \n \n \n \n\n\n \n Cui, X.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 58, McMaster University, Hamilton, Ontario, Canada, July 2009.\n URL: http://www.cas.mcmaster.ca/sqrl/papers/SQRLreport58.pdf\n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{CuiSekerinski09ABC,\n\taddress = {Hamilton, Ontario, Canada},\n\ttype = {{SQRL} {Report}},\n\ttitle = {An {Experimental} {Implementation} of {Action}-{Based} {Concurrency}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/CuiSekerinski09ABC.pdf},\n\tabstract = {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.},\n\tnumber = {58},\n\tinstitution = {McMaster University},\n\tauthor = {Cui, Xiao-lei and Sekerinski, Emil},\n\tmonth = jul,\n\tyear = {2009},\n\tnote = {URL: http://www.cas.mcmaster.ca/sqrl/papers/SQRLreport58.pdf},\n\tpages = {27},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Algebraic Approach to Refinement with Fair Choice.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Boiten, E.; Derrick, J.; and Schellhorn, G., editor(s), Proceedings of the 13th BAC-FACS Refinement Workshop (REFINE 2008), volume 214, of Electronic Notes in Theoretical Computer Science, pages 51–79, June 2008. \n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski08AlgebraicFairChoice,\n\tseries = {Electronic {Notes} in {Theoretical} {Computer} {Science}},\n\ttitle = {An {Algebraic} {Approach} to {Refinement} with {Fair} {Choice}},\n\tvolume = {214},\n\tdoi = {http://dx.doi.org/10.1016/j.entcs.2008.06.004},\n\tabstract = {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.},\n\tbooktitle = {Proceedings of the 13th {BAC}-{FACS} {Refinement} {Workshop} ({REFINE} 2008)},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Boiten, E. and Derrick, J. and Schellhorn, G.},\n\tmonth = jun,\n\tyear = {2008},\n\tkeywords = {refinement, action systems, alternating bit protocol, fairness},\n\tpages = {51--79},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verifying Statecharts with State Invariants.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Breitman, K.; Woodcock, J.; Sterritt, R.; and Hinchey, M., editor(s), 13th IEEE International Conference on Engineering of Complex Computer Systems, of ICECCS '08, pages 7–14, Belfast, Northern Ireland, March 2008. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski08StateInvariants,\n\taddress = {Belfast, Northern Ireland},\n\tseries = {{ICECCS} '08},\n\ttitle = {Verifying {Statecharts} with {State} {Invariants}},\n\tdoi = {http://dx.doi.org/10.1109/ICECCS.2008.40},\n\tabstract = {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.},\n\tbooktitle = {13th {IEEE} {International} {Conference} on {Engineering} of {Complex} {Computer} {Systems}},\n\tpublisher = {IEEE Computer Society},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Breitman, K. and Woodcock, J. and Sterritt, R. and Hinchey, M.},\n\tmonth = mar,\n\tyear = {2008},\n\tpages = {7--14},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Teaching the Unifying Mathematics of Software Design.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Technical Report 49, McMaster University, Hamilton, Ontario, Canada, December 2007.\n \n\n\n\n
\n\n\n\n \n \n \"TeachingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{Sekerinski07TeachingSoftwareDesign,\n\taddress = {Hamilton, Ontario, Canada},\n\ttype = {{SQRL} {Report}},\n\ttitle = {Teaching the {Unifying} {Mathematics} of {Software} {Design}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski07TeachingSoftwareDesign.pdf},\n\tabstract = {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.},\n\tnumber = {49},\n\tinstitution = {McMaster University},\n\tauthor = {Sekerinski, Emil},\n\tmonth = dec,\n\tyear = {2007},\n\tpages = {17},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n FM 2006: Formal Methods–14th International Symposium on Formal Methods.\n \n \n \n\n\n \n Misra, J.; Nipkow, T.; and Sekerinski, E.,\n editors.\n \n\n\n \n\n\n\n Volume 4085 of Lecture Notes in Computer ScienceSpringer, Hamilton, Ontario, Canada, August 2006.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{MisraNipkowSekerinski06FormalMethods,\n\taddress = {Hamilton, Ontario, Canada},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {{FM} 2006: {Formal} {Methods}–14th {International} {Symposium} on {Formal} {Methods}},\n\tvolume = {4085},\n\tpublisher = {Springer},\n\teditor = {Misra, Jayadev and Nipkow, Tobias and Sekerinski, Emil},\n\tmonth = aug,\n\tyear = {2006},\n\tdoi = {10.1007/11813040},\n\tannote = {ISSN 0302-9743 (Print) 1611-3349 (Online) DOI 10.1007/11813040 ISBN 978-3-540-37215-8},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Teaching the Mathematics of Software Design.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Boute, R. T.; and Oliveira, J. N., editor(s), Formal Methods in the Teaching Lab, Workshop at the FM 2006: Formal Methods Symposium, pages 53–58, August 2006. \n \n\n\n\n
\n\n\n\n \n \n \"TeachingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski06TeachingSoftwareDesign,\n\ttitle = {Teaching the {Mathematics} of {Software} {Design}},\n\turl = {http://www4.di.uminho.pt/FME-SoE/FMEd06/},\n\tabstract = {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.},\n\tbooktitle = {Formal {Methods} in the {Teaching} {Lab}, {Workshop} at the {FM} 2006: {Formal} {Methods} {Symposium}},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Boute, R. T. and Oliveira, J. N.},\n\tmonth = aug,\n\tyear = {2006},\n\tpages = {53--58},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Topics in Software Design. Volume 2.\n \n \n \n \n\n\n \n Sekerinski, E.,\n editor.\n \n\n\n \n\n\n\n SQRL Report 35, June 2006.\n \n\n\n\n
\n\n\n\n \n \n \"TopicsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{Sekerinski06SoftwareDesign2,\n\ttitle = {Topics in {Software} {Design}. {Volume} 2},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski06SoftwareDesign2.pdf},\n\tabstract = {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.},\n\tpublisher = {SQRL Report 35},\n\teditor = {Sekerinski, Emil},\n\tmonth = jun,\n\tyear = {2006},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Statechart Verification with iState.\n \n \n \n \n\n\n \n Le, D. T. M.; Sekerinski, E.; and West, S.\n\n\n \n\n\n\n In Chechik, M., editor(s), FM 2006: Formal Methods–Posters and Research Tools, pages 1–6, Hamilton, Ontario, Canada, August 2006. \n \n\n\n\n
\n\n\n\n \n \n \"StatechartPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{LeSekerinskiWest06StatechartVerification,\n\taddress = {Hamilton, Ontario, Canada},\n\ttitle = {Statechart {Verification} with {iState}},\n\turl = {http://fm06.mcmaster.ca/istate.pdf},\n\tbooktitle = {{FM} 2006: {Formal} {Methods}–{Posters} and {Research} {Tools}},\n\tauthor = {Le, Dai Tri Man and Sekerinski, Emil and West, Scott},\n\teditor = {Chechik, Marsha},\n\tmonth = aug,\n\tyear = {2006},\n\tpages = {1--6},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2005\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Topics in Software Design. Volume 1.\n \n \n \n \n\n\n \n Sekerinski, E.,\n editor.\n \n\n\n \n\n\n\n SQRL Report 34, June 2005.\n \n\n\n\n
\n\n\n\n \n \n \"TopicsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{Sekerinski05SoftwareDesign1,\n\ttitle = {Topics in {Software} {Design}. {Volume} 1},\n\tcopyright = {http://sqrl.mcmaster.ca/sqrl\\_reports.html},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski05SoftwareDesign1.pdf},\n\tabstract = {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.},\n\tpublisher = {SQRL Report 34},\n\teditor = {Sekerinski, Emil},\n\tmonth = jun,\n\tyear = {2005},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verification and Refinement with Fine-Grained Action-Based Concurrent Objects.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Theoretical Computer Science, 331(2–3): 429–455. February 2005.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{Sekerinski05ConcurrentObjects,\n\ttitle = {Verification and {Refinement} with {Fine}-{Grained} {Action}-{Based} {Concurrent} {Objects}},\n\tvolume = {331},\n\tdoi = {10.1016/j.tcs.2004.09.024},\n\tabstract = {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.},\n\tnumber = {2–3},\n\tjournal = {Theoretical Computer Science},\n\tauthor = {Sekerinski, Emil},\n\tmonth = feb,\n\tyear = {2005},\n\tpages = {429--455},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Integrating Specification and Documentation in an Object-oriented Language.\n \n \n \n \n\n\n \n Liang, J.; and Sekerinski, E.\n\n\n \n\n\n\n In SAVCBS 2004, Specification and Verification of Component-Based Systems, of Workshop of SIGSOFT 2004/FSE-12, 12th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 126–129, Newport Beach, California, USA, November 2004. Technical Report #04-09, Department of Computer Science, Iowa State University\n \n\n\n\n
\n\n\n\n \n \n \"IntegratingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{LiangSekerinski04IntegratingSpecificationDocumentation,\n\taddress = {Newport Beach, California, USA},\n\tseries = {Workshop of {SIGSOFT} 2004/{FSE}-12, 12th {ACM} {SIGSOFT} {Symposium} on the {Foundations} of {Software} {Engineering}},\n\ttitle = {Integrating {Specification} and {Documentation} in an {Object}-oriented {Language}},\n\turl = {https://www.cs.ucf.edu/~leavens/SAVCBS/2004/savcbs04.pdf},\n\tabstract = {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].},\n\tbooktitle = {{SAVCBS} 2004, {Specification} and {Verification} of {Component}-{Based} {Systems}},\n\tpublisher = {Technical Report \\#04-09, Department of Computer Science, Iowa State University},\n\tauthor = {Liang, Jie and Sekerinski, Emil},\n\tmonth = nov,\n\tyear = {2004},\n\tpages = {126--129},\n\tannote = {October 31-November 5 4 pages (double column)},\n}\n\n
\n
\n\n\n
\n 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].\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2003\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Exploring Tabular Verification and Refinement.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Formal Aspects of Computing, 15(2): 215–236. November 2003.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{Sekerinski03TabularVerificationRefinement,\n\ttitle = {Exploring {Tabular} {Verification} and {Refinement}},\n\tvolume = {15},\n\tdoi = {10.1007/s00165-003-0010-9},\n\tabstract = {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.},\n\tnumber = {2},\n\tjournal = {Formal Aspects of Computing},\n\tauthor = {Sekerinski, Emil},\n\tmonth = nov,\n\tyear = {2003},\n\tpages = {215--236},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Simple Model for Concurrent Object-Oriented Programming.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Milutinovic, V., editor(s), International Conference Internet, Processing, Systems, Interdisciplinaries, IPSI 2003, pages 1–4, Sveti Stefan, Montenegro, October 2003. \n Editor:\n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski03SimpleCOOP,\n\taddress = {Sveti Stefan, Montenegro},\n\ttitle = {A {Simple} {Model} for {Concurrent} {Object}-{Oriented} {Programming}},\n\tcopyright = {http://vipsi.org/ipsi/conferences/},\n\tabstract = {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.},\n\tbooktitle = {International {Conference} {Internet}, {Processing}, {Systems}, {Interdisciplinaries}, {IPSI} 2003},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Milutinovic, Veljko},\n\tmonth = oct,\n\tyear = {2003},\n\tnote = {Editor:},\n\tpages = {1--4},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Concurrent Object-Oriented Programs: From Specification to Code.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Boer, F. S. d.; Bonsangue, M.; Graf, S.; and Roever, W. d., editor(s), Formal Methods for Components and Objects, First International Symposium, FMCO 02, volume 2852, of Lecture Notes in Computer Science, pages 403–423, Leiden, The Netherlands, July 2003. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski03COOP,\n\taddress = {Leiden, The Netherlands},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Concurrent {Object}-{Oriented} {Programs}: {From} {Specification} to {Code}},\n\tvolume = {2852},\n\tdoi = {10.1007/978-3-540-39656-7_17},\n\tabstract = {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.},\n\tbooktitle = {Formal {Methods} for {Components} and {Objects}, {First} {International} {Symposium}, {FMCO} 02},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Boer, F. S. de and Bonsangue, M. and Graf, S. and Roever, W.-P. de},\n\tmonth = jul,\n\tyear = {2003},\n\tpages = {403--423},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2002\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Tabular Verification and Refinement.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Derrick, J.; Boiten, E.; Woodcock, J.; and Wright, J. v., editor(s), REFINE 2002, The BCS FACS Refinement Workshop, volume 70, of Electronic Notes in Theoretical Computer Science, pages 179–198, July 2002. Elsevier\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski02TabularVerificationRefinement,\n\tseries = {Electronic {Notes} in {Theoretical} {Computer} {Science}},\n\ttitle = {Tabular {Verification} and {Refinement}},\n\tvolume = {70},\n\tdoi = {10.1016/S1571-0661(05)80492-X},\n\tabstract = {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.},\n\tbooktitle = {{REFINE} 2002, {The} {BCS} {FACS} {Refinement} {Workshop}},\n\tpublisher = {Elsevier},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Derrick, John and Boiten, Eerke and Woodcock, Jim and Wright, Joakim von},\n\tmonth = jul,\n\tyear = {2002},\n\tpages = {179--198},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Translating Statecharts to B.\n \n \n \n\n\n \n Sekerinski, E.; and Zurob, R.\n\n\n \n\n\n\n In Butler, M.; Petre, L.; and Sere, K., editor(s), Third International Conference on Integrated Formal Methods, volume 2335, of Lecture Notes in Computer Science, pages 128–144, Turku, Finland, May 2002. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{SekerinskiZurob02StatechartsToB,\n\taddress = {Turku, Finland},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Translating {Statecharts} to {B}},\n\tvolume = {2335},\n\tdoi = {10.1007/3-540-47884-1_8},\n\tabstract = {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.},\n\tbooktitle = {Third {International} {Conference} on {Integrated} {Formal} {Methods}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil and Zurob, Rafik},\n\teditor = {Butler, Michael and Petre, Luigia and Sere, Kaisa},\n\tmonth = may,\n\tyear = {2002},\n\tpages = {128--144},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2001\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Foundations of the Trace Assertion Method of Module Interface Specification.\n \n \n \n\n\n \n Janicki, R.; and Sekerinski, E.\n\n\n \n\n\n\n IEEE Transactions on Software Engineering, 27(7): 577–598. July 2001.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n 
@article{JanickiSekerinski01TraceAssertion,\n\ttitle = {Foundations of the {Trace} {Assertion} {Method} of {Module} {Interface} {Specification}},\n\tvolume = {27},\n\tissn = {0098-5589},\n\tdoi = {10.1109/32.935852},\n\tabstract = {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.},\n\tnumber = {7},\n\tjournal = {IEEE Transactions on Software Engineering},\n\tauthor = {Janicki, Ryszard and Sekerinski, Emil},\n\tmonth = jul,\n\tyear = {2001},\n\tkeywords = {nondeterminism, Mealy machines, Module interface specifications, module refinement, relational model, state machines, step-sequences, tabular notation., trace assertion method},\n\tpages = {577--598},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n iState: A Statechart Translator.\n \n \n \n\n\n \n Sekerinski, E.; and Zurob, R.\n\n\n \n\n\n\n In Gogolla, M.; and Kobryn, C., editor(s), «UML» 2001 – The Unified Modeling Language, 4th International Conference, volume 2185, of Lecture Notes in Computer Science, pages 376–390, Toronto, Canada, October 2001. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{SekerinskiZurob01iState,\n\taddress = {Toronto, Canada},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {{iState}: {A} {Statechart} {Translator}},\n\tvolume = {2185},\n\tdoi = {10.1007/3-540-45441-1_28},\n\tabstract = {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.},\n\tbooktitle = {«{UML}» 2001 – {The} {Unified} {Modeling} {Language}, 4th {International} {Conference}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil and Zurob, Rafik},\n\teditor = {Gogolla, Martin and Kobryn, Cris},\n\tmonth = oct,\n\tyear = {2001},\n\tpages = {376--390},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n From Statecharts to Code: A Tool for the Graphical Design of Reactive Systems.\n \n \n \n\n\n \n Sekerinski, E.; and Zurob, R.\n\n\n \n\n\n\n Technical Report McMaster University, 2001.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{SekerinskiZurob01StatechartsToCode,\n\ttype = {{CAS} {Technical} {Report}},\n\ttitle = {From {Statecharts} to {Code}: {A} {Tool} for the {Graphical} {Design} of {Reactive} {Systems}},\n\tinstitution = {McMaster University},\n\tauthor = {Sekerinski, Emil and Zurob, Rafik},\n\tyear = {2001},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2000\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Foundation for Refining Concurrent Objects.\n \n \n \n \n\n\n \n Büchi, M.; and Sekerinski, E.\n\n\n \n\n\n\n Fundamenta Informaticae, 44(1,2): 25–61. September 2000.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{BuchiSekerinski00RefiningConcurrentObjects,\n\ttitle = {A {Foundation} for {Refining} {Concurrent} {Objects}},\n\tvolume = {44},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/BuchiSekerinski00RefiningConcurrentObjectsPreprint.pdf},\n\tabstract = {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.},\n\tnumber = {1,2},\n\tjournal = {Fundamenta Informaticae},\n\tauthor = {Büchi, Martin and Sekerinski, Emil},\n\tmonth = sep,\n\tyear = {2000},\n\tpages = {25--61},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Guarded Commands with Fair Choice.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Backhouse, R.; and Oliveira, J., editor(s), 5th International Conference on the Mathematics of Program Construction, MPC 2000, volume 1837, of Lecture Notes in Computer Science, pages 127–139, Ponte de Lima, Portugal, July 2000. Springer-Verlag\n CitationKey: Sekerinski00FairChoice\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski00FairChoice,\n\taddress = {Ponte de Lima, Portugal},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {On {Guarded} {Commands} with {Fair} {Choice}},\n\tvolume = {1837},\n\tdoi = {10.1007/10722010_9},\n\tabstract = {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.},\n\tbooktitle = {5th {International} {Conference} on the {Mathematics} of {Program} {Construction}, {MPC} 2000},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Backhouse, Roland and Oliveira, Jose},\n\tmonth = jul,\n\tyear = {2000},\n\tnote = {CitationKey: Sekerinski00FairChoice},\n\tpages = {127--139},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1999\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Refining Concurrent Objects.\n \n \n \n \n\n\n \n Büchi, M.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 298, Turku Centre for Computer Science, August 1999.\n \n\n\n\n
\n\n\n\n \n \n \"RefiningPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@techreport{BuchiSekerinski99RefiningConcurrentObjects,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {Refining {Concurrent} {Objects}},\n\turl = {http://tucs.fi/publications/view/?pub_id=tBuSe99a},\n\tabstract = {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.},\n\tnumber = {298},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Büchi, Martin and Sekerinski, Emil},\n\tmonth = aug,\n\tyear = {1999},\n\tkeywords = {ISBN 952-12-0509-1 ISSN 1239-1891},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Ensuring Correctness of Java Frameworks: A Formal Look at JCF.\n \n \n \n \n\n\n \n Mikhajlova, A.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 250, TUCS, March 1999.\n \n\n\n\n
\n\n\n\n \n \n \"EnsuringPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{MikhajlovaSekerinski99CorrectnessJavaFrameworks,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {Ensuring {Correctness} of {Java} {Frameworks}: {A} {Formal} {Look} at {JCF}},\n\turl = {http://tucs.fi/publications/view/?pub_id=tMiSe99a},\n\tabstract = {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.},\n\tnumber = {250},\n\tinstitution = {TUCS},\n\tauthor = {Mikhajlova, Anna and Sekerinski, Emil},\n\tmonth = mar,\n\tyear = {1999},\n\tannote = {ISBN 952-12-0402-8 ISSN 1239-1891},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Developing Components in Presence of Re-entrance.\n \n \n \n\n\n \n Mikhajlov, L.; Sekerinski, E.; and Laibinis, L.\n\n\n \n\n\n\n In Wing, J.; Woodcock, J.; and Davis, J., editor(s), FM'99 — Formal Methods, volume 1709, of Lecture Notes in Computer Science, pages 721–721, Toulouse, France, September 1999. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MikhajlovSekerinskiLaibinis99ComponentsReentrance,\n\taddress = {Toulouse, France},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Developing {Components} in {Presence} of {Re}-entrance},\n\tvolume = {1709},\n\tdoi = {10.1007/3-540-48118-4_19},\n\tabstract = {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.},\n\tbooktitle = {{FM}'99 — {Formal} {Methods}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Mikhajlov, Leonid and Sekerinski, Emil and Laibinis, Linas},\n\teditor = {Wing, Jeanette and Woodcock, Jim and Davis, Jim},\n\tmonth = sep,\n\tyear = {1999},\n\tpages = {721--721},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Developing Components in Presence of Re-entrance.\n \n \n \n \n\n\n \n Mikhajlov, L.; Sekerinski, E.; and Laibinis, L.\n\n\n \n\n\n\n Technical Report 239, Turku Centre for Computer Science, February 1999.\n \n\n\n\n
\n\n\n\n \n \n \"DevelopingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@techreport{MikhajlovSekerinskiLaibinis99ComponentsReentranceReport,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {Developing {Components} in {Presence} of {Re}-entrance},\n\turl = {http://tucs.fi/publications/view/?pub_id=tMiSeLa99a},\n\tabstract = {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.},\n\tnumber = {239},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Mikhajlov, Leonid and Sekerinski, Emil and Laibinis, Linas},\n\tmonth = feb,\n\tyear = {1999},\n\tkeywords = {ISBN 952-12-0382-X ISSN 1239-1891},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Foundations of the Trace Assertion Method of Module Interface Specification.\n \n \n \n \n\n\n \n Janicki, R.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 376, McMaster University, July 1999.\n \n\n\n\n
\n\n\n\n \n \n \"FoundationsPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{JanickiSekerinski99TraceAssertion,\n\ttype = {{SERG} {Report}},\n\ttitle = {Foundations of the {Trace} {Assertion} {Method} of {Module} {Interface} {Specification}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/JanickiSekerinski99TraceAssertion.pdf},\n\tabstract = {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.},\n\tnumber = {376},\n\tinstitution = {McMaster University},\n\tauthor = {Janicki, Ryszard and Sekerinski, Emil},\n\tmonth = jul,\n\tyear = {1999},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1998\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Formal Methods for Component Software: The Refinement Calculus Perspective.\n \n \n \n\n\n \n Büchi, M.; and Sekerinski, E.\n\n\n \n\n\n\n In Bosch, J.; and Mitchell, S., editor(s), Object-Oriented Technology–ECOOP '97 Workshop Reader, volume 1357, of Lecture Notes in Computer Science, pages 332–337, May 1998. Springer\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{BuchiSekerinski98ComponentsRefinement,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Formal {Methods} for {Component} {Software}: {The} {Refinement} {Calculus} {Perspective}},\n\tvolume = {1357},\n\tdoi = {10.1007/3-540-69687-3_68},\n\tabstract = {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.},\n\tbooktitle = {Object-{Oriented} {Technology}–{ECOOP} '97 {Workshop} {Reader}},\n\tpublisher = {Springer},\n\tauthor = {Büchi, Martin and Sekerinski, Emil},\n\teditor = {Bosch, Jan and Mitchell, Stuart},\n\tmonth = may,\n\tyear = {1998},\n\tpages = {332--337},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Production Cell.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Sekerinski, E.; and Sere, K., editor(s), Program Development by Stepwise Refinement: Case Studies Using the B Method, of Formal Approaches to Computing and Information Technology Series, pages 197–254. Springer-Verlag, 1998.\n \n\n\n\n
\n\n\n\n \n \n \"ProductionPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{Sekerinski98ProductionCell,\n\tseries = {Formal {Approaches} to {Computing} and {Information} {Technology} {Series}},\n\ttitle = {Production {Cell}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiSere98CaseStudiesB.pdf},\n\tabstract = {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.\nThe 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.},\n\tbooktitle = {Program {Development} by {Stepwise} {Refinement}: {Case} {Studies} {Using} the {B} {Method}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Sekerinski, Emil and Sere, Kaisa},\n\tyear = {1998},\n\tpages = {197--254},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Program Development by Stepwise Refinement: Case Studies Using the B Method.\n \n \n \n \n\n\n \n Sekerinski, E.; and Sere, K.,\n editors.\n \n\n\n \n\n\n\n of Formal Approaches to Computing and Information TechnologySpringer-Verlag, 1998.\n \n\n\n\n
\n\n\n\n \n \n \"ProgramPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@book{SekerinskiSere98CaseStudiesB,\n\tseries = {Formal {Approaches} to {Computing} and {Information} {Technology}},\n\ttitle = {Program {Development} by {Stepwise} {Refinement}: {Case} {Studies} {Using} the {B} {Method}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/SekerinskiSere98CaseStudiesB.pdf},\n\tabstract = {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.},\n\tpublisher = {Springer-Verlag},\n\teditor = {Sekerinski, Emil and Sere, Kaisa},\n\tyear = {1998},\n\tdoi = {10.1007/978-1-4471-0585-5},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Study of the Fragile Base Class Problem.\n \n \n \n\n\n \n Mikhajlov, L.; and Sekerinski, E.\n\n\n \n\n\n\n In Jul, E., editor(s), ECOOP'98 — 12th European Conference on Object-Oriented Programming, volume 1445, of Lecture Notes in Computer Science, pages 355–382, Brussels, Belgium, July 1998. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MikhajlovSekerinski98FragileBaseClassProblem,\n\taddress = {Brussels, Belgium},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {A {Study} of the {Fragile} {Base} {Class} {Problem}},\n\tvolume = {1445},\n\tdoi = {10.1007/BFb0054099},\n\tabstract = {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.},\n\tbooktitle = {{ECOOP}'98 — 12th {European} {Conference} on {Object}-{Oriented} {Programming}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Mikhajlov, Leonid and Sekerinski, Emil},\n\teditor = {Jul, Eric},\n\tmonth = jul,\n\tyear = {1998},\n\tpages = {355--382},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Graphical Design of Reactive Systems.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Bert, D., editor(s), B'98: Recent Advances in the Development and Use of the B Method, volume 1393, of Lecture Notes in Computer Science, pages 182–197, April 1998. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski98GraphicalDesignReactiveSystem,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Graphical {Design} of {Reactive} {Systems}},\n\tvolume = {1393},\n\tdoi = {10.1007/BFb0053361},\n\tabstract = {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.},\n\tbooktitle = {B'98: {Recent} {Advances} in the {Development} and {Use} of the {B} {Method}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Bert, Didier},\n\tmonth = apr,\n\tyear = {1998},\n\tpages = {182--197},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1997\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Class Refinement and Interface Refinement in Object-Oriented Development.\n \n \n \n \n\n\n \n Mikhajlova, A.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report Turku Centre for Computer Science, March 1997.\n \n\n\n\n
\n\n\n\n \n \n \"ClassPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{MikhajlovaSekerinski97ClassInterfaceRefinementReport,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {Class {Refinement} and {Interface} {Refinement} in {Object}-{Oriented} {Development}},\n\turl = {http://tucs.fi/publications/view/?pub_id=tMiSe97},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Mikhajlova, Anna and Sekerinski, Emil},\n\tmonth = mar,\n\tyear = {1997},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Methods for Component Software: The Refinement Calculus Perspective.\n \n \n \n \n\n\n \n Büchi, M.; and Sekerinski, E.\n\n\n \n\n\n\n In Weck, W.; Bosch, J.; and Szyperski, C., editor(s), Second Workshop on Component-Oriented Programming (WCOP), volume 5, pages 23–32, Jyväskylä, Finland, September 1997. TUCS General Publication\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{BuchiSekerinski97Components,\n\taddress = {Jyväskylä, Finland},\n\ttitle = {Formal {Methods} for {Component} {Software}: {The} {Refinement} {Calculus} {Perspective}},\n\tvolume = {5},\n\turl = {https://tucs.fi/publications/view/?pub_id=bWeBoSzy97},\n\tabstract = {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.},\n\tbooktitle = {Second {Workshop} on {Component}-{Oriented} {Programming} ({WCOP})},\n\tpublisher = {TUCS General Publication},\n\tauthor = {Büchi, Martin and Sekerinski, Emil},\n\teditor = {Weck, Wolfgang and Bosch, Jan and Szyperski, Clemens},\n\tmonth = sep,\n\tyear = {1997},\n\tpages = {23--32},\n\tannote = {This paper is available in 3 versions of different length. The version presented at the workshop in compressed PostScript format (40 KB, ftp://ftp.abo.fi/pub/cs/papers/mbuechi/FMforCS.ps.gz), the revised and slightly shortened version in the TUCS WCOP proceedings in compressed PostScript format (63 KB, ftp://ftp.abo.fi/pub/cs/papers/mbuechi/FMforCSTUCS.ps.gz), and the brief summary which appeared in the LNCS workshop reader in compressed PostScript format (18 KB, ftp://ftp.abo.fi/pub/cs/papers/mbuechi/FMforCSLNCS.ps.gz). The slides of this talk in compressed PostScript format (122 KB, ftp://ftp.abo.fi/pub/cs/papers/mbuechi/FMforCSSlides.ps.gz)},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Class Refinement and Interface Refinement in Object-Oriented Programs.\n \n \n \n \n\n\n \n Mikhajlova, A.; and Sekerinski, E.\n\n\n \n\n\n\n In Fitzgerald, J.; Jones, C.; and Lucas, P., editor(s), FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, volume 1313, of Lecture Notes in Computer Science, pages 82–101, Graz, Austria, September 1997. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"ClassPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MikhajlovaSekerinski97ClassInterfaceRefinement,\n\taddress = {Graz, Austria},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Class {Refinement} and {Interface} {Refinement} in {Object}-{Oriented} {Programs}},\n\tvolume = {1313},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/MikhajlovaSekerinski97ClassInterfaceRefinement.pdf},\n\tdoi = {10.1007/3-540-63533-5_5},\n\tabstract = {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.},\n\tbooktitle = {{FME} '97: {Industrial} {Applications} and {Strengthened} {Foundations} of {Formal} {Methods}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Mikhajlova, Anna and Sekerinski, Emil},\n\teditor = {Fitzgerald, John and Jones, Cliff and Lucas, Peter},\n\tmonth = sep,\n\tyear = {1997},\n\tpages = {82--101},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Fragile Base Class Problem and Its Solution.\n \n \n \n \n\n\n \n Mikhajlov, L.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 117, Turku Centre for Computer Science, May 1997.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@techreport{MikhajlovSekerinski97FBCPSolution,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {The {Fragile} {Base} {Class} {Problem} and {Its} {Solution}},\n\turl = {http://tucs.fi/publications/view/?pub_id=tLMiSe97},\n\tabstract = {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.},\n\tnumber = {117},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Mikhajlov, Leonid and Sekerinski, Emil},\n\tmonth = may,\n\tyear = {1997},\n\tkeywords = {ISBN 952-12-0020-0 ISSN 1239-1891 32 pages},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Fragile Base Class Problem and Its Impact on Component Systems.\n \n \n \n\n\n \n Mikhajlov, L.; and Sekerinski, E.\n\n\n \n\n\n\n In Weck, W.; Bosch, J.; and Szyperski, C., editor(s), Second Workshop on Component-Oriented Programming (WCOP), volume 5, of TUCS General Publication, pages 59–68, Jyväskylä, Finland, September 1997. Turku Centre for Computer Science\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MikhajlovSekerinski97FBCPImpact,\n\taddress = {Jyväskylä, Finland},\n\tseries = {{TUCS} {General} {Publication}},\n\ttitle = {The {Fragile} {Base} {Class} {Problem} and {Its} {Impact} on {Component} {Systems}},\n\tvolume = {5},\n\tdoi = {10.1007/3-540-69687-3_72},\n\tabstract = {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.},\n\tbooktitle = {Second {Workshop} on {Component}-{Oriented} {Programming} ({WCOP})},\n\tpublisher = {Turku Centre for Computer Science},\n\tauthor = {Mikhajlov, Leonid and Sekerinski, Emil},\n\teditor = {Weck, Wolfgang and Bosch, Jan and Szyperski, Clemens},\n\tmonth = sep,\n\tyear = {1997},\n\tpages = {59--68},\n\tannote = {http://www.abo.fi/ wweck/WCOP97/},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1996\n \n \n (11)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n An Action System Approach to the Steam Boiler Problem.\n \n \n \n \n\n\n \n Butler, M.; Sekerinski, E.; and Sere, K.\n\n\n \n\n\n\n In Abrial, J.; Börger, E.; and Langmaack, H., editor(s), Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, volume 1165, of Lecture Notes in Computer Science, pages 129–148, October 1996. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{ButlerSekerinskiSere96SteamBoiler,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {An {Action} {System} {Approach} to the {Steam} {Boiler} {Problem}},\n\tvolume = {1165},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/ButlerSekerinskiSere96SteamBoiler.pdf},\n\tdoi = {10.1007/BFb0027234},\n\tabstract = {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.},\n\tbooktitle = {Formal {Methods} for {Industrial} {Applications}: {Specifying} and {Programming} the {Steam} {Boiler} {Control}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Butler, Michael and Sekerinski, Emil and Sere, Kaisa},\n\teditor = {Abrial, Jean-Raymond and Börger, Egon and Langmaack, Hans},\n\tmonth = oct,\n\tyear = {1996},\n\tpages = {129--148},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Description of Object-Oriented Design Patterns.\n \n \n \n \n\n\n \n Back, R.; Mikhajlov, L.; and Sekerinski, E.\n\n\n \n\n\n\n In 8th Nordic Workshop on Programming Theory, Oslo, Norway, December 1996. \n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{BackMikhailovSekerinski96FormalDesignPatterns,\n\taddress = {Oslo, Norway},\n\ttitle = {Formal {Description} of {Object}-{Oriented} {Design} {Patterns}},\n\turl = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no:80/~nwpt96/},\n\tabstract = {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.},\n\tbooktitle = {8th {Nordic} {Workshop} on {Programming} {Theory}},\n\tauthor = {Back, Ralph and Mikhajlov, Leonid and Sekerinski, Emil},\n\tmonth = dec,\n\tyear = {1996},\n\tannote = {http://www.ifi.uio.no/ nwpt96/},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Adding Type-Bound Actions to Action-Oberon.\n \n \n \n \n\n\n \n Back, R.; Büchi, M.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report 66, Turku Centre for Computer Science, November 1996.\n \n\n\n\n
\n\n\n\n \n \n \"AddingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{BackBuchiSekerinski96TypeBoundActions,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {Adding {Type}-{Bound} {Actions} to {Action}-{Oberon}},\n\turl = {http://www.tucs.fi/Publications/techreports/TR66.php},\n\tabstract = {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.},\n\tnumber = {66},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Back, Ralph and Büchi, Martin and Sekerinski, Emil},\n\tmonth = nov,\n\tyear = {1996},\n\tannote = {ISBN 951-650-891-X ISSN 1239-1891 15 pages},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Stepwise Development of Object-Oriented Programs with Interface Refinement.\n \n \n \n \n\n\n \n Back, R. J.; Mikhaljova, A.; and Sekerinski, E.\n\n\n \n\n\n\n In Nordic Workshop on Program Correctness, Oslo, December 1996. \n \n\n\n\n
\n\n\n\n \n \n \"StepwisePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{BackMikhailovaSekerinski96StepwiseInterfaceRefinement,\n\taddress = {Oslo},\n\ttitle = {Stepwise {Development} of {Object}-{Oriented} {Programs} with {Interface} {Refinement}},\n\turl = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no:80/~nwpt96/},\n\tbooktitle = {Nordic {Workshop} on {Program} {Correctness}},\n\tauthor = {Back, R. J. and Mikhaljova, A. and Sekerinski, E.},\n\tmonth = dec,\n\tyear = {1996},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Class Refinement and Interface Refinement in Object-Oriented Development.\n \n \n \n \n\n\n \n Mikhajlova, A.; and Sekerinski, E.\n\n\n \n\n\n\n In 8th Nordic Workshop on Programming Theory, Oslo, Norway, December 1996. \n \n\n\n\n
\n\n\n\n \n \n \"ClassPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{MikhailovaSekerinski96ClassInterfaceRefinement,\n\taddress = {Oslo, Norway},\n\ttitle = {Class {Refinement} and {Interface} {Refinement} in {Object}-{Oriented} {Development}},\n\turl = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no:80/~nwpt96/},\n\tbooktitle = {8th {Nordic} {Workshop} on {Programming} {Theory}},\n\tauthor = {Mikhajlova, Anna and Sekerinski, Emil},\n\tmonth = dec,\n\tyear = {1996},\n\tannote = {http://www.abo.fi/ amikhajl/Papers/publications.html},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Theory of Prioritizing Composition.\n \n \n \n\n\n \n Sekerinski, E.; and Sere, K.\n\n\n \n\n\n\n The Computer Journal, 39(8): 701–712. August 1996.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@article{SekerinskiSere96PrioritizingComposition,\n\ttitle = {A {Theory} of {Prioritizing} {Composition}},\n\tvolume = {39},\n\tdoi = {10.1093/comjnl/39.8.701},\n\tabstract = {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.},\n\tnumber = {8},\n\tjournal = {The Computer Journal},\n\tauthor = {Sekerinski, Emil and Sere, Kaisa},\n\tmonth = aug,\n\tyear = {1996},\n\tpages = {701--712},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Probabilities in Action Systems.\n \n \n \n \n\n\n \n Sekerinski, E.; Sere, K.; and Troubitsyna, E.\n\n\n \n\n\n\n In 8th Nordic Workshop on Programming Theory, Oslo, Norway, December 1996. \n \n\n\n\n
\n\n\n\n \n \n \"ProbabilitiesPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{SekerinskiSereTroubitsyna96ProbabilitiesActionSystems,\n\taddress = {Oslo, Norway},\n\ttitle = {Probabilities in {Action} {Systems}},\n\turl = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no/~nwpt96/},\n\tabstract = {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.},\n\tbooktitle = {8th {Nordic} {Workshop} on {Programming} {Theory}},\n\tauthor = {Sekerinski, Emil and Sere, Kaisa and Troubitsyna, Elena},\n\tmonth = dec,\n\tyear = {1996},\n\tannote = {http://www.ifi.uio.no/ nwpt96/},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Theory of Prioritising Composition.\n \n \n \n \n\n\n \n Sekerinski, E.; and Sere, K.\n\n\n \n\n\n\n Technical Report 5, Turku Centre for Computer Science, May 1996.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{SekerinskiSere96PrioritisingCompositionReport,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {A {Theory} of {Prioritising} {Composition}},\n\turl = {https://tucs.fi/publications/view/?pub_id=tSS96},\n\tabstract = {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.},\n\tnumber = {5},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Sekerinski, Emil and Sere, Kaisa},\n\tmonth = may,\n\tyear = {1996},\n\tannote = {ISBN 951-650-741-7},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Deriving Control Programs by Weakest Preconditions.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Technical Report 4, Turku Centre for Computer Science, April 1996.\n \n\n\n\n
\n\n\n\n \n \n \"DerivingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{Sekerinski96ControlProgramWeakestPreconditions,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {Deriving {Control} {Programs} by {Weakest} {Preconditions}},\n\turl = {http://tucs.fi/publications/view/?pub_id=tSekerinski96},\n\tabstract = {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.},\n\tnumber = {4},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Sekerinski, Emil},\n\tmonth = apr,\n\tyear = {1996},\n\tannote = {ISBN 951-650-740-9},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Type-Theoretic Basis for an Object-Oriented Refinement Calculus.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Goldsack, S. J.; and Kent, S. J. H., editor(s), Formal Methods and Object Technology, pages 317–335, 1996. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski96TypeTheoreticObjectOrientedRefinement,\n\ttitle = {A {Type}-{Theoretic} {Basis} for an {Object}-{Oriented} {Refinement} {Calculus}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski96TypeTheoreticObjectOrientedRefinement.pdf},\n\tabstract = {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.},\n\tbooktitle = {Formal {Methods} and {Object} {Technology}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Goldsack, Stephen J. and Kent, Stuart J. H.},\n\tyear = {1996},\n\tkeywords = {10.1007/978-1-4471-3071-0\\_15},\n\tpages = {317--335},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Control Systems as Action Systems.\n \n \n \n \n\n\n \n Rönkkö, M.; Sekerinski, E.; and Sere, K.\n\n\n \n\n\n\n In Smedinga, R.; Spathopoulos, M. P.; and Kozák, P., editor(s), WODES 96 – Workshop on Discrete Event Systems, pages 362–367, Edinburgh, August 1996. Institute of Electronical Engineers\n \n\n\n\n
\n\n\n\n \n \n \"ControlPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{RonkkoSekerinskiSere96ControlActionSystems,\n\taddress = {Edinburgh},\n\ttitle = {Control {Systems} as {Action} {Systems}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/RonkkoSekerinskiSere96ControlActionSystems.pdf},\n\tabstract = {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.},\n\tbooktitle = {{WODES} 96 – {Workshop} on {Discrete} {Event} {Systems}},\n\tpublisher = {Institute of Electronical Engineers},\n\tauthor = {Rönkkö, Mauno and Sekerinski, Emil and Sere, Kaisa},\n\teditor = {Smedinga, R. and Spathopoulos, M. P. and Kozák, P.},\n\tmonth = aug,\n\tyear = {1996},\n\tpages = {362--367},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1995\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n An Action System Approach to the Steam Boiler Problem.\n \n \n \n \n\n\n \n Butler, M.; Sekerinski, E.; and Sere, K.\n\n\n \n\n\n\n In Abrial, J.; Börger, E.; and Langmaack, H., editor(s), Methods for Semantics and Specification, volume 117, of Dagstuhl Seminiar-Report, June 1995. \n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{ButlerSekerinskiSere95SteamBoilerDagstuhl,\n\tseries = {Dagstuhl {Seminiar}-{Report}},\n\ttitle = {An {Action} {System} {Approach} to the {Steam} {Boiler} {Problem}},\n\tvolume = {117},\n\turl = {http://www.dagstuhl.de/9523},\n\tbooktitle = {Methods for {Semantics} and {Specification}},\n\tauthor = {Butler, Michael and Sekerinski, Emil and Sere, Kaisa},\n\teditor = {Abrial, J.-R. and Börger, E. and Langmaack, H.},\n\tmonth = jun,\n\tyear = {1995},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An Action System Approach to the Steam Boiler Problem.\n \n \n \n \n\n\n \n Butler, M.; Sekerinski, E.; and Sere, K.\n\n\n \n\n\n\n Technical Report Turku Centre for Computer Science, 1995.\n \n\n\n\n
\n\n\n\n \n \n \"AnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{ButlerSekerinskiSere95SteamBoiler,\n\ttype = {{TUCS} {Technical} {Report}},\n\ttitle = {An {Action} {System} {Approach} to the {Steam} {Boiler} {Problem}},\n\turl = {http://tucs.fi/publications/view/?pub_id=tBuSeSe95},\n\tabstract = {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.},\n\tinstitution = {Turku Centre for Computer Science},\n\tauthor = {Butler, Michael and Sekerinski, Emil and Sere, Kaisa},\n\tyear = {1995},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n RAISE: A Rigorous Approach Using Stepwise Refinement.\n \n \n \n\n\n \n Erasmy, F.; and Sekerinski, E.\n\n\n \n\n\n\n In Lewerentz, C.; and Lindner, T., editor(s), Formal Development of Reactive Systems – Case Study Production Cell, volume 891, of Lecture Notes in Computer Science, pages 277–293, 1995. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{ErasmySekerinski95RAISE,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {{RAISE}: {A} {Rigorous} {Approach} {Using} {Stepwise} {Refinement}},\n\tvolume = {891},\n\tdoi = {10.1007/3-540-58867-1_60},\n\tabstract = {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.},\n\tbooktitle = {Formal {Development} of {Reactive} {Systems} – {Case} {Study} {Production} {Cell}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Erasmy, F. and Sekerinski, E.},\n\teditor = {Lewerentz, C. and Lindner, Th.},\n\tyear = {1995},\n\tpages = {277--293},\n\tannote = {ISBN 3-540-58867-1},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Object-Oriented Design and Verification.\n \n \n \n\n\n \n Lewerentz, C.; Lindner, T.; Rüping, A.; and Sekerinski, E.\n\n\n \n\n\n\n In Broy, M.; and Jähnichen, S., editor(s), KORSO: Methods, Languages, and Tools for the Construction of Correct Software, volume 1009, of Lecture Notes in Computer Science, pages 92–111, 1995. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{LewerentzLindnerRupingSekerinski95OODesignVerification,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {On {Object}-{Oriented} {Design} and {Verification}},\n\tvolume = {1009},\n\tdoi = {10.1007/BFb0015457},\n\tabstract = {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.},\n\tbooktitle = {{KORSO}: {Methods}, {Languages}, and {Tools} for the {Construction} of {Correct} {Software}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Lewerentz, C. and Lindner, T. and Rüping, A. and Sekerinski, E.},\n\teditor = {Broy, Manfred and Jähnichen, Stefan},\n\tyear = {1995},\n\tpages = {92--111},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Object-Oriented Design and Verification.\n \n \n \n\n\n \n Lewerentz, C.; Lindner, T.; Rüping, A.; and Sekerinski, E.\n\n\n \n\n\n\n In Casais, E., editor(s), Architectures and Processes for Systematic Software Construction, volume 1, pages 27–51. FZI Publication, 1995.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{LewerentzLindnerRupingSekerinski95OODesignVerificationReport,\n\ttitle = {On {Object}-{Oriented} {Design} and {Verification}},\n\tvolume = {1},\n\tbooktitle = {Architectures and {Processes} for {Systematic} {Software} {Construction}},\n\tpublisher = {FZI Publication},\n\tauthor = {Lewerentz, C. and Lindner, T. and Rüping, A. and Sekerinski, E.},\n\teditor = {Casais, E.},\n\tyear = {1995},\n\tpages = {27--51},\n\tannote = {ISSN 0944-3037},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Modula-3: Modelling and Implementation.\n \n \n \n\n\n \n Rüping, A.; and Sekerinski, E.\n\n\n \n\n\n\n In Lewerentz, C.; and Lindner, T., editor(s), Formal Development of Reactive Systems - Case Study Production Cell, volume 891, of Lecture Notes in Computer Science, pages 357–371. Springer-Verlag, 1995.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{rupingModula3ModellingImplementation1995,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Modula-3: {Modelling} and {Implementation}},\n\tvolume = {891},\n\tabstract = {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.},\n\tbooktitle = {Formal {Development} of {Reactive} {Systems} - {Case} {Study} {Production} {Cell}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Rüping, A. and Sekerinski, E.},\n\teditor = {Lewerentz, C. and Lindner, Th.},\n\tyear = {1995},\n\tdoi = {10.1007/3-540-58867-1_64},\n\tpages = {357--371},\n\tannote = {ISBN 540-58867-1},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1994\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Stepwise Refinement of Control Software - A Case Study using RAISE.\n \n \n \n\n\n \n Erasmy, F.; and Sekerinski, E.\n\n\n \n\n\n\n In Naftalin, M.; Denvir, T.; and Bertran, M., editor(s), FME'94: Industrial Benefit of Formal Methods, volume 873, of Lecture Notes in Computer Science, pages 547–566, Barcelona, Spain, October 1994. Springer-Verlag\n CitationKey: ErasmySekerinski94ControlRefinement\n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{ErasmySekerinski94ControlRefinement,\n\taddress = {Barcelona, Spain},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Stepwise {Refinement} of {Control} {Software} - {A} {Case} {Study} using {RAISE}},\n\tvolume = {873},\n\tdoi = {10.1007/3-540-58555-9_115},\n\tbooktitle = {{FME}'94: {Industrial} {Benefit} of {Formal} {Methods}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Erasmy, F. and Sekerinski, E.},\n\teditor = {Naftalin, M. and Denvir, T. and Bertran, M.},\n\tmonth = oct,\n\tyear = {1994},\n\tnote = {CitationKey: ErasmySekerinski94ControlRefinement},\n\tpages = {547--566},\n\tannote = {ISBN 3-540-58555-9},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n RAISE: A Rigorous Approach Towards the Production Cell Using Stepwise Refinement.\n \n \n \n\n\n \n Erasmy, F.; and Sekerinski, E.\n\n\n \n\n\n\n In Lewerentz, C.; and Lindner, T., editor(s), Case Study “Production Cell”—A Comparative Study in Formal Software Development, volume 1, pages 155–172. FZI Publication, 1994.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{ErasmySekerinski95RAISE,\n\ttitle = {{RAISE}: {A} {Rigorous} {Approach} {Towards} the {Production} {Cell} {Using} {Stepwise} {Refinement}},\n\tvolume = {1},\n\tbooktitle = {Case {Study} “{Production} {Cell}”—{A} {Comparative} {Study} in {Formal} {Software} {Development}},\n\tpublisher = {FZI Publication},\n\tauthor = {Erasmy, F. and Sekerinski, E.},\n\teditor = {Lewerentz, C. and Lindner, Th.},\n\tyear = {1994},\n\tpages = {155--172},\n\tannote = {ISSN 0944-3037},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Verfeinerung in der Objektorientierten Programmkonstruktion.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Ph.D. Thesis, University of Karlsruhe, 1994.\n \n\n\n\n
\n\n\n\n \n \n \"VerfeinerungPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@phdthesis{Sekerinski94VerfeinerungOOP,\n\ttype = {Dissertation},\n\ttitle = {Verfeinerung in der {Objektorientierten} {Programmkonstruktion}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski94VerfeinerungOOP.pdf},\n\tabstract = {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:\n• Implementieren von Klassen\n• Inkrementelles Modifizieren von Klassen durch Vererbung\n• Herausfaktorisieren von Gemeinsamkeiten von Klassen\nEs werden Beweis- und Konstruktionsregeln für die korrekte Anwendung dieser Entwurfsprinzipien aufgestellt. Die Regeln tragen auch zu einem tieferen Verständnis der Entwurfsprinzipien bei.\nSpezifikationen haben die Form von indeterministischen Anweisungen, wie sie\naus dem Verfeinerungskalkül bekannt sind, bei denen das Resultat durch ein\nPrädikat spezifiziert wird. An objektorientierten Konzepten werden Objekte mit\nAttributen und Methoden, Kapselung privater Attribute, Klassen mit Vererbung,\nUntertyp-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.\nDas 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.},\n\tschool = {University of Karlsruhe},\n\tauthor = {Sekerinski, Emil},\n\tyear = {1994},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Modula-3: The Modelling and Implementation of an Industrial Production Cell.\n \n \n \n\n\n \n Rüping, A.; and Sekerinski, E.\n\n\n \n\n\n\n In Lewerentz, C.; and Lindner, T., editor(s), Case Study Production Cell - A Comparative Study in Formal Software Development, volume 1, pages 357–371. FZI Publication, 1994.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@incollection{RupingSekerinski95Modula3,\n\ttitle = {Modula-3: {The} {Modelling} and {Implementation} of an {Industrial} {Production} {Cell}},\n\tvolume = {1},\n\tbooktitle = {Case {Study} {Production} {Cell} - {A} {Comparative} {Study} in {Formal} {Software} {Development}},\n\tpublisher = {FZI Publication},\n\tauthor = {Rüping, A. and Sekerinski, E.},\n\teditor = {Lewerentz, C. and Lindner, Th.},\n\tyear = {1994},\n\tpages = {357--371},\n\tannote = {ISSN 0944-3037},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1993\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n The Process of Formal Object-Oriented Software Development.\n \n \n \n\n\n \n Casais, E.; Lewerentz, C.; Rüping, A.; Sekerinski, E.; and Weber, F.,\n editors.\n \n\n\n \n\n\n\n Technical Report Forschungszentrum Informatik Karlsruhe, March 1993.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{CasaisEtAl93FormalObjectOrientedDevelopment,\n\ttype = {{FZI} {Bericht}},\n\ttitle = {The {Process} of {Formal} {Object}-{Oriented} {Software} {Development}},\n\tinstitution = {Forschungszentrum Informatik Karlsruhe},\n\teditor = {Casais, Eduardo and Lewerentz, Claus and Rüping, Andreas and Sekerinski, Emil and Weber, Franz},\n\tmonth = mar,\n\tyear = {1993},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Behavioural View of Object Types.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Technical Report 7/93, Forschungszentrum Informatik, March 1993.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{Sekerinski93BehaviouralObjectTypes,\n\ttype = {{FZI} {Bericht}},\n\ttitle = {A {Behavioural} {View} of {Object} {Types}},\n\tnumber = {7/93},\n\tinstitution = {Forschungszentrum Informatik},\n\tauthor = {Sekerinski, Emil},\n\tmonth = mar,\n\tyear = {1993},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Calculus for Predicative Programming.\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Bird, R. S.; Morgan, C. C.; and Woodcock, J. C. P., editor(s), Mathematics of Program Construction, volume 669, of Lecture Notes in Computer Science, pages 302–321, Oxford, U.K., February 1993. Springer-Verlag\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski93PredicativeProgramming,\n\taddress = {Oxford, U.K.},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {A {Calculus} for {Predicative} {Programming}},\n\tvolume = {669},\n\tdoi = {10.1007/3-540-56625-2_20},\n\tabstract = {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.},\n\tbooktitle = {Mathematics of {Program} {Construction}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Bird, R. S. and Morgan, C. C. and Woodcock, J. C. P.},\n\tmonth = feb,\n\tyear = {1993},\n\tkeywords = {ISBN 3-540-56625-2},\n\tpages = {302--321},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Refinement Algebra for Object-Oriented Programming (extended abstact).\n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n In Goldsack, S.; and Kent, S., editor(s), BCS Workshop on Formal Aspects of Object-Oriented Systems, London, 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@inproceedings{Sekerinski93RefinementAlgebraOOP,\n\taddress = {London},\n\ttitle = {Refinement {Algebra} for {Object}-{Oriented} {Programming} (extended abstact)},\n\tbooktitle = {{BCS} {Workshop} on {Formal} {Aspects} of {Object}-{Oriented} {Systems}},\n\tauthor = {Sekerinski, E.},\n\teditor = {Goldsack, S. and Kent, S.},\n\tyear = {1993},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1992\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Objektorientierte Spezifikationsmethoden.\n \n \n \n\n\n \n Lewerentz, C.; Rüping, A.; Sekerinski, E.; and Weber, F.,\n editors.\n \n\n\n \n\n\n\n Technical Report 29, Forschungszentrum Informatik, April 1992.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{LewerentzEtAl92Spezifikationsmethoden,\n\ttype = {{FZI} {Bericht}},\n\ttitle = {Objektorientierte {Spezifikationsmethoden}},\n\tnumber = {29},\n\tinstitution = {Forschungszentrum Informatik},\n\teditor = {Lewerentz, C. and Rüping, A. and Sekerinski, E. and Weber, F.},\n\tmonth = apr,\n\tyear = {1992},\n\tpages = {100},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1991\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Software-Wiederverwendung.\n \n \n \n\n\n \n Neumann, D.; Sekerinski, E.; Tick, J.; and Weber, F.,\n editors.\n \n\n\n \n\n\n\n Technical Report 27, Forschungszentrum Informatik, November 1991.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{NeumannEtAlSoftwareWiederverwendung,\n\ttype = {{FZI} {Bericht}},\n\ttitle = {Software-{Wiederverwendung}},\n\tnumber = {27},\n\tinstitution = {Forschungszentrum Informatik},\n\teditor = {Neumann, D. and Sekerinski, E. and Tick, J. and Weber, F.},\n\tmonth = nov,\n\tyear = {1991},\n\tpages = {65},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Softwareproduktionsumgebungen.\n \n \n \n\n\n \n Kienhöfer, J.; Rehm, S.; and Sekerinski, E.,\n editors.\n \n\n\n \n\n\n\n Technical Report 22, Forschungszentrum Informatik, May 1991.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{KienhoferRehmSekerinski91Softwareproduktionsumgebungen,\n\ttype = {{FZI} {Bericht}},\n\ttitle = {Softwareproduktionsumgebungen},\n\tnumber = {22},\n\tinstitution = {Forschungszentrum Informatik},\n\teditor = {Kienhöfer, J. and Rehm, S. and Sekerinski, E.},\n\tmonth = may,\n\tyear = {1991},\n\tpages = {71},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Object Management System of Stone – OBST Release 3.0.\n \n \n \n\n\n \n Uhl, J.; Theobald, D.; Schiefer, B.; Sekerinski, E.; Rehm, S.; and Ranft, M.\n\n\n \n\n\n\n Technical Report Forschungszentrum Informatik, February 1991.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{UhlEtAl91OBST,\n\ttype = {{FZI} {Publikation}},\n\ttitle = {The {Object} {Management} {System} of {Stone} – {OBST} {Release} 3.0},\n\tinstitution = {Forschungszentrum Informatik},\n\tauthor = {Uhl, J. and Theobald, D. and Schiefer, B. and Sekerinski, E. and Rehm, S. and Ranft, M.},\n\tmonth = feb,\n\tyear = {1991},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1990\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Formale Methoden der Softwareentwicklung.\n \n \n \n\n\n \n Uhl, J.; and Sekerinski, E.,\n editors.\n \n\n\n \n\n\n\n Technical Report 18, Forschungszentrum Informatik, June 1990.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{UhlSekerinski90FormaleSoftwareentwicklung,\n\ttype = {{FZI} {Bericht}},\n\ttitle = {Formale {Methoden} der {Softwareentwicklung}},\n\tnumber = {18},\n\tinstitution = {Forschungszentrum Informatik},\n\teditor = {Uhl, J. and Sekerinski, E.},\n\tmonth = jun,\n\tyear = {1990},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The Object Management of Stone – System Design and Implementation.\n \n \n \n\n\n \n Uhl, J.; Schiefer, B.; and Sekerinski, E.\n\n\n \n\n\n\n Technical Report Forschungszentrum Informatik, October 1990.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@techreport{UhlEtAl90ObjectManagement,\n\ttype = {{FZI} {Publikation}},\n\ttitle = {The {Object} {Management} of {Stone} – {System} {Design} and {Implementation}},\n\tinstitution = {Forschungszentrum Informatik},\n\tauthor = {Uhl, J. and Schiefer, B. and Sekerinski, E.},\n\tmonth = oct,\n\tyear = {1990},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1989\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Entwicklung eines korrekten Assemblierers.\n \n \n \n \n\n\n \n Sekerinski, E.\n\n\n \n\n\n\n Ph.D. Thesis, Universität Karlsruhe, 1989.\n \n\n\n\n
\n\n\n\n \n \n \"EntwicklungPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n 
@phdthesis{Sekerinski89,\n\ttype = {Diplomarbeit},\n\ttitle = {Entwicklung eines korrekten {Assemblierers}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski89.pdf},\n\tabstract = {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.},\n\tschool = {Universität Karlsruhe},\n\tauthor = {Sekerinski, Emil},\n\tyear = {1989},\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);