People
Research Groups:
More Info
Ivan José Varzinczak is a professor of computer science at Univ. d'Artois and member of CRIL Lab France. He holds a Ph.D. (2006) in Artificial Intelligence from Université Paul Sabatier, France, an M.Sc. (2002) and a B.Sc. (2000) both in Computer Science from the Federal University of Paraná, Brazil.
Ivan’s main research interest area is logic-based knowledge representation and reasoning in artificial intelligence, with focus on modal and description logics and their applications in non-monotonic reasoning, reasoning about actions and change, and the semantic web.
Ivan’s main research interest area is logic-based knowledge representation and reasoning in artificial intelligence, with focus on modal and description logics and their applications in non-monotonic reasoning, reasoning about actions and change, and the semantic web.
Latest Research Publications:
1.
Casini G, Meyer T, Varzinczak I. Contextual Conditional Reasoning. In: 35th AAAI Conference on Artificial Intelligence. Online: AAAI Press; 2021.
We extend the expressivity of classical conditional reasoning by introducing context as a new parameter. The enriched
conditional logic generalises the defeasible conditional setting in the style of Kraus, Lehmann, and Magidor, and allows for a refined semantics that is able to distinguish, for example, between expectations and counterfactuals. In this paper we introduce the language for the enriched logic and define an appropriate semantic framework for it. We analyse which properties generally associated with conditional reasoning are still satisfied by the new semantic framework, provide a suitable representation result, and define an entailment relation based on Lehmann and Magidor’s generally-accepted notion of Rational Closure.
@{430,
author = {Giovanni Casini, Tommie Meyer, Ivan Varzinczak},
title = {Contextual Conditional Reasoning},
abstract = {We extend the expressivity of classical conditional reasoning by introducing context as a new parameter. The enriched
conditional logic generalises the defeasible conditional setting in the style of Kraus, Lehmann, and Magidor, and allows for a refined semantics that is able to distinguish, for example, between expectations and counterfactuals. In this paper we introduce the language for the enriched logic and define an appropriate semantic framework for it. We analyse which properties generally associated with conditional reasoning are still satisfied by the new semantic framework, provide a suitable representation result, and define an entailment relation based on Lehmann and Magidor’s generally-accepted notion of Rational Closure.},
year = {2021},
journal = {35th AAAI Conference on Artificial Intelligence},
pages = {6254-6261},
month = {02/02/2021-09/02/2021},
publisher = {AAAI Press},
address = {Online},
}
1.
Britz K, Casini G, Meyer T, Moodley K, Sattler U, Varzinczak I. Principles of KLM-style Defeasible Description Logics. Transactions on Computational Logic. 2020;22 (1). doi:10.1145/3420258.
The past 25 years have seen many attempts to introduce defeasible-reasoning capabilities into a description logic setting. Many, if not most, of these attempts are based on preferential extensions of description logics, with a significant number of these, in turn, following the so-called KLM approach to defeasible reasoning initially advocated for propositional logic by Kraus, Lehmann, and Magidor. Each of these attempts has its own aim of investigating particular constructions and variants of the (KLM-style) preferential approach. Here our aim is to provide a comprehensive study of the formal foundations of preferential defeasible reasoning for description logics in the KLM tradition. We start by investigating a notion of defeasible subsumption in the spirit of defeasible conditionals as studied by Kraus, Lehmann, and Magidor in the propositional case. In particular, we consider a natural and intuitive semantics for defeasible subsumption, and we investigate KLM-style syntactic properties for both preferential and rational subsumption. Our contribution includes two representation results linking our semantic
constructions to the set of preferential and rational properties considered. Besides showing that our semantics is appropriate, these results pave the way for more effective decision procedures for defeasible reasoning in description logics. Indeed, we also analyse the problem of non-monotonic reasoning in description logics at the level of entailment and present an algorithm for the computation of rational closure of a defeasible knowledge base. Importantly, our algorithm relies completely on classical entailment and shows that the computational complexity of reasoning over defeasible knowledge bases is no worse than that of reasoning in the underlying classical DL ALC.
@article{433,
author = {Katarina Britz, Giovanni Casini, Tommie Meyer, Kody Moodley, Uli Sattler, Ivan Varzinczak},
title = {Principles of KLM-style Defeasible Description Logics},
abstract = {The past 25 years have seen many attempts to introduce defeasible-reasoning capabilities into a description logic setting. Many, if not most, of these attempts are based on preferential extensions of description logics, with a significant number of these, in turn, following the so-called KLM approach to defeasible reasoning initially advocated for propositional logic by Kraus, Lehmann, and Magidor. Each of these attempts has its own aim of investigating particular constructions and variants of the (KLM-style) preferential approach. Here our aim is to provide a comprehensive study of the formal foundations of preferential defeasible reasoning for description logics in the KLM tradition. We start by investigating a notion of defeasible subsumption in the spirit of defeasible conditionals as studied by Kraus, Lehmann, and Magidor in the propositional case. In particular, we consider a natural and intuitive semantics for defeasible subsumption, and we investigate KLM-style syntactic properties for both preferential and rational subsumption. Our contribution includes two representation results linking our semantic
constructions to the set of preferential and rational properties considered. Besides showing that our semantics is appropriate, these results pave the way for more effective decision procedures for defeasible reasoning in description logics. Indeed, we also analyse the problem of non-monotonic reasoning in description logics at the level of entailment and present an algorithm for the computation of rational closure of a defeasible knowledge base. Importantly, our algorithm relies completely on classical entailment and shows that the computational complexity of reasoning over defeasible knowledge bases is no worse than that of reasoning in the underlying classical DL ALC.},
year = {2020},
journal = {Transactions on Computational Logic},
volume = {22 (1)},
pages = {1-46},
publisher = {ACM},
url = {https://dl-acm-org.ezproxy.uct.ac.za/doi/abs/10.1145/3420258},
doi = {10.1145/3420258},
}
1.
Casini G, Meyer T, Varzinczak I. Rational Defeasible Belief Change. In: 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020). Virtual: IJCAI; 2020. doi:10.24963/kr.2020/22.
We present a formal framework for modelling belief change within a non-monotonic reasoning system. Belief change and non-monotonic reasoning are two areas that are formally closely related, with recent attention being paid towards the analysis of belief change within a non-monotonic environment. In this paper we consider the classical AGM belief change operators, contraction and revision, applied to a defeasible setting in the style of Kraus, Lehmann, and Magidor. The investigation leads us to the formal characterisation of a number of classes of defeasible belief change operators. For the most interesting classes we need to consider the problem of iterated belief change, generalising the classical work of Darwiche and Pearl in the process. Our work involves belief change operators aimed at ensuring logical consistency, as well as the characterisation of analogous operators aimed at obtaining coherence—an important notion within the field of logic-based ontologies
@{382,
author = {Giovanni Casini, Tommie Meyer, Ivan Varzinczak},
title = {Rational Defeasible Belief Change},
abstract = {We present a formal framework for modelling belief change within a non-monotonic reasoning system. Belief change and non-monotonic reasoning are two areas that are formally closely related, with recent attention being paid towards the analysis of belief change within a non-monotonic environment. In this paper we consider the classical AGM belief change operators, contraction and revision, applied to a defeasible setting in the style of Kraus, Lehmann, and Magidor. The investigation leads us to the formal characterisation of a number of classes of defeasible belief change operators. For the most interesting classes we need to consider the problem of iterated belief change, generalising the classical work of Darwiche and Pearl in the process. Our work involves belief change operators aimed at ensuring logical consistency, as well as the characterisation of analogous operators aimed at obtaining coherence—an important notion within the field of logic-based ontologies},
year = {2020},
journal = {17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020)},
pages = {213-222},
month = {12/09/2020},
publisher = {IJCAI},
address = {Virtual},
url = {https://library.confdna.com/kr/2020/},
doi = {10.24963/kr.2020/22},
}
1.
Britz K, Varzinczak I. Preferential tableaux for contextual defeasible ALC. In: 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). Springer LNAI no. 11714; 2019. https://www.springer.com/gp/book/9783030290252.
In recent work, we addressed an important limitation in previous ex- tensions of description logics to represent defeasible knowledge, namely the re- striction in the semantics of defeasible concept inclusion to a single preference or- der on objects of the domain. Syntactically, this limitation translates to a context- agnostic notion of defeasible subsumption, which is quite restrictive when it comes to modelling different nuances of defeasibility. Our point of departure in our recent proposal allows for different orderings on the interpretation of roles. This yields a notion of contextual defeasible subsumption, where the context is informed by a role. In the present paper, we extend this work to also provide a proof-theoretic counterpart and associated results. We define a (naïve) tableau- based algorithm for checking preferential consistency of contextual defeasible knowledge bases, a central piece in the definition of other forms of contextual defeasible reasoning over ontologies, notably contextual rational closure.
@{247,
author = {Katarina Britz, Ivan Varzinczak},
title = {Preferential tableaux for contextual defeasible ALC},
abstract = {In recent work, we addressed an important limitation in previous ex- tensions of description logics to represent defeasible knowledge, namely the re- striction in the semantics of defeasible concept inclusion to a single preference or- der on objects of the domain. Syntactically, this limitation translates to a context- agnostic notion of defeasible subsumption, which is quite restrictive when it comes to modelling different nuances of defeasibility. Our point of departure in our recent proposal allows for different orderings on the interpretation of roles. This yields a notion of contextual defeasible subsumption, where the context is informed by a role. In the present paper, we extend this work to also provide a proof-theoretic counterpart and associated results. We define a (naïve) tableau- based algorithm for checking preferential consistency of contextual defeasible knowledge bases, a central piece in the definition of other forms of contextual defeasible reasoning over ontologies, notably contextual rational closure.},
year = {2019},
journal = {28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)},
pages = {39-57},
month = {03/09-05/09},
publisher = {Springer LNAI no. 11714},
isbn = {ISBN 978-3-030-29026-9},
url = {https://www.springer.com/gp/book/9783030290252},
}
1.
Britz K, Varzinczak I. Contextual rational closure for defeasible ALC. Annals of Mathematics and Artificial Intelligence. 2019;87(1-2). doi:10.1007/s10472-019-09658-2.
Description logics have been extended in a number of ways to support defeasible reason- ing in the KLM tradition. Such features include preferential or rational defeasible concept inclusion, and defeasible roles in complex concept descriptions. Semantically, defeasible subsumption is obtained by means of a preference order on objects, while defeasible roles are obtained by adding a preference order to role interpretations. In this paper, we address an important limitation in defeasible extensions of description logics, namely the restriction in the semantics of defeasible concept inclusion to a single preference order on objects. We do this by inducing a modular preference order on objects from each modular preference order on roles, and using these to relativise defeasible subsumption. This yields a notion of contextualised rational defeasible subsumption, with contexts described by roles. We also provide a semantic construction for rational closure and a method for its computation, and present a correspondence result between the two.
@article{246,
author = {Katarina Britz, Ivan Varzinczak},
title = {Contextual rational closure for defeasible ALC},
abstract = {Description logics have been extended in a number of ways to support defeasible reason- ing in the KLM tradition. Such features include preferential or rational defeasible concept inclusion, and defeasible roles in complex concept descriptions. Semantically, defeasible subsumption is obtained by means of a preference order on objects, while defeasible roles are obtained by adding a preference order to role interpretations. In this paper, we address an important limitation in defeasible extensions of description logics, namely the restriction in the semantics of defeasible concept inclusion to a single preference order on objects. We do this by inducing a modular preference order on objects from each modular preference order on roles, and using these to relativise defeasible subsumption. This yields a notion of contextualised rational defeasible subsumption, with contexts described by roles. We also provide a semantic construction for rational closure and a method for its computation, and present a correspondence result between the two.},
year = {2019},
journal = {Annals of Mathematics and Artificial Intelligence},
volume = {87},
pages = {83-108},
issue = {1-2},
isbn = {ISSN: 1012-2443},
url = {https://link.springer.com/article/10.1007/s10472-019-09658-2},
doi = {10.1007/s10472-019-09658-2},
}
Research Groups:
More Info
Tezira is Pursuing her PhD in the Adaptive and Cognitive Systems Lab at the University of Cape Town. Her research is on Designing and Evaluating an Agent-based Architecture for Automatic Knowledge Discovery and Evolution. She is also an Assistant Lecturer at Mbarara University of Science and Technology in the Department of Computer Science, Faculty of Computing and Informatics.
Latest Research Publications:
1.
Wanyana T, Nzomo M, Price CS, Moodley D. Combining Machine Learning and Bayesian Networks for ECG Interpretation and Explanation. In: Proceedings of the 8th International Conference on Information and Communication Technologies for Ageing Well and e-Health - ICT4AWE. INSTICC: SciTePress; 2022. doi:https://doi.org/10.5220/0011046100003188.
We explore how machine learning (ML) and Bayesian networks (BNs) can be combined in a personal health agent (PHA) for the detection and interpretation of electrocardiogram (ECG) characteristics. We propose a PHA that uses ECG data from wearables to monitor heart activity, and interprets and explains the observed readings. We focus on atrial fibrillation (AF), the commonest type of arrhythmia. The absence of a P-wave in an ECG is the hallmark indication of AF. Four ML models are trained to classify an ECG signal based on the presence or absence of the P-wave: multilayer perceptron (MLP), logistic regression, support vector machine, and random forest. The MLP is the best performing model with an accuracy of 89.61% and an F1 score of 88.68%. A BN representing AF risk factors is developed based on expert knowledge from the literature and evaluated using Pitchforth and Mengersen’s validation framework. The P-wave presence or absence as determined by the ML model is input into the BN. The PHA is evaluated using sample use cases to illustrate how the BN can explain the occurrence of AF using diagnostic reasoning. This gives the most likely AF risk factors for the individual
@inbook{478,
author = {Tezira Wanyana, Mbithe Nzomo, C. Sue Price, Deshen Moodley},
title = {Combining Machine Learning and Bayesian Networks for ECG Interpretation and Explanation},
abstract = {We explore how machine learning (ML) and Bayesian networks (BNs) can be combined in a personal health agent (PHA) for the detection and interpretation of electrocardiogram (ECG) characteristics. We propose a PHA that uses ECG data from wearables to monitor heart activity, and interprets and explains the observed readings. We focus on atrial fibrillation (AF), the commonest type of arrhythmia. The absence of a P-wave in an ECG is the hallmark indication of AF. Four ML models are trained to classify an ECG signal based on the presence or absence of the P-wave: multilayer perceptron (MLP), logistic regression, support vector machine, and random forest. The MLP is the best performing model with an accuracy of 89.61% and an F1 score of 88.68%. A BN representing AF risk factors is developed based on expert knowledge from the literature and evaluated using Pitchforth and Mengersen’s validation framework. The P-wave presence or absence as determined by the ML model is input into the BN. The PHA is evaluated using sample use cases to illustrate how the BN can explain the occurrence of AF using diagnostic reasoning. This gives the most likely AF risk factors for the individual},
year = {2022},
journal = {Proceedings of the 8th International Conference on Information and Communication Technologies for Ageing Well and e-Health - ICT4AWE},
pages = {81-92},
publisher = {SciTePress},
address = {INSTICC},
isbn = {978-989-758-566-1},
doi = {https://doi.org/10.5220/0011046100003188},
}
1.
Wanyana T, Moodley D. An Agent Architecture for Knowledge Discovery and Evolution. In: KI 2021: Advances in Artificial Intelligence. volume 12873. Cham: Springer International Publishing; 2021. doi:https://doi.org/10.1007/978-3-030-87626-5_18.
The abductive theory of method (ATOM) was recently proposed to describe the process that scientists use for knowledge discovery. In this paper we propose an agent architecture for knowledge discovery and evolution (KDE) based on ATOM. The agent incorporates a combination of ontologies, rules and Bayesian networks for representing different aspects of its internal knowledge. The agent uses an external AI service to detect unexpected situations from incoming observations. It then uses rules to analyse the current situation and a Bayesian network for finding plausible explanations for unexpected situations. The architecture is evaluated and analysed on a use case application for monitoring daily household electricity consumption patterns.
@inbook{425,
author = {Tezira Wanyana, Deshen Moodley},
title = {An Agent Architecture for Knowledge Discovery and Evolution},
abstract = {The abductive theory of method (ATOM) was recently proposed to describe the process that scientists use for knowledge discovery. In this paper we propose an agent architecture for knowledge discovery and evolution (KDE) based on ATOM. The agent incorporates a combination of ontologies, rules and Bayesian networks for representing different aspects of its internal knowledge. The agent uses an external AI service to detect unexpected situations from incoming observations. It then uses rules to analyse the current situation and a Bayesian network for finding plausible explanations for unexpected situations. The architecture is evaluated and analysed on a use case application for monitoring daily household electricity consumption patterns.},
year = {2021},
journal = {KI 2021: Advances in Artificial Intelligence},
edition = {volume 12873},
pages = {241-256},
publisher = {Springer International Publishing},
address = {Cham},
isbn = {978-3-030-87626-5},
doi = {https://doi.org/10.1007/978-3-030-87626-5_18},
}
1.
Wanyana T, Moodley D, Meyer T. An Ontology for Supporting Knowledge Discovery and Evolution. In: First Southern African Conference for Artificial Intelligence Research. Virtual: SACAIR2020; 2020. https://2020.sacair.org.za/wp-content/uploads/2021/02/SACAIR_Proceedings-MainBook_Finv4_compressed.pdf?_ga=2.116601743.849395099.1621802506-572599210.1621419278.
Knowledge Discovery and Evolution (KDE) is of interest to a broad array of researchers from both Philosophy of Science (PoS) and Artificial Intelligence (AI), in particular, Knowledge Representation and Reasoning (KR), Machine Learning and Data Mining (ML-DM) and the Agent Based Systems (ABS) communities. In PoS, Haig recently pro- posed a so-called broad theory of scientific method that uses abduction for generating theories to explain phenomena. He refers to this method of scientific inquiry as the Abductive Theory of Method (ATOM). In this paper, we analyse ATOM, align it with KR and ML-DM perspectives and propose an algorithm and an ontology for supporting agent based knowledge discovery and evolution based on ATOM. We illustrate the use of the algorithm and the ontology on a use case application for electricity consumption behaviour in residential households.
@{405,
author = {Tezira Wanyana, Deshen Moodley, Tommie Meyer},
title = {An Ontology for Supporting Knowledge Discovery and Evolution},
abstract = {Knowledge Discovery and Evolution (KDE) is of interest to a broad array of researchers from both Philosophy of Science (PoS) and Artificial Intelligence (AI), in particular, Knowledge Representation and Reasoning (KR), Machine Learning and Data Mining (ML-DM) and the Agent Based Systems (ABS) communities. In PoS, Haig recently pro- posed a so-called broad theory of scientific method that uses abduction for generating theories to explain phenomena. He refers to this method of scientific inquiry as the Abductive Theory of Method (ATOM). In this paper, we analyse ATOM, align it with KR and ML-DM perspectives and propose an algorithm and an ontology for supporting agent based knowledge discovery and evolution based on ATOM. We illustrate the use of the algorithm and the ontology on a use case application for electricity consumption behaviour in residential households.},
year = {2020},
journal = {First Southern African Conference for Artificial Intelligence Research},
pages = {206-221},
month = {22/02/2021},
publisher = {SACAIR2020},
address = {Virtual},
isbn = {978-0-620-89373-2},
url = {https://2020.sacair.org.za/wp-content/uploads/2021/02/SACAIR_Proceedings-MainBook_Finv4_compressed.pdf?_ga=2.116601743.849395099.1621802506-572599210.1621419278},
}
More Info
DEGREES LINKED TO THIS GROUP:
2019-Current PhD (Humanities): 'A Critical Inquiry into the Metaphysics for Mind Uploading'.
2019-Current PhD (Humanities): 'A Critical Inquiry into the Metaphysics for Mind Uploading'.
Latest Research Publications:
No Results
Research Groups:
More Info
Latest Research Publications:
1.
Daykin J, Groult R, Guesnet Y, Lecroq T, Lefebvre A, Leonard M, Mouchard L, Prieur-Gaston E, Watson B. Efficient pattern matching in degenerate strings with the Burrows–Wheeler transform. Information Processing Letters. 2019;147. doi:https://doi.org/10.1016/j.ipl.2019.03.003.
A degenerate or indeterminate string on an alphabet SIGMA is a sequence of non-empty subsets of SIGMA . Given a degenerate string t of length n and its Burrows–Wheeler transform we present a new method for searching for a degenerate pattern of length m in t running in O ( mn ) time on a constant size alphabet SIGMA. Furthermore, it is a hybrid pattern matching technique that works on both regular and degenerate strings. A degenerate string is said to be conservative if its number of non-solid letters is upper-bounded by a fixed positive constant q; in this case we show that the search time complexity is O ( qm^2 ) for counting
the number of occurrences and O ( qm^2 + occ ) for reporting the found occurrences where occ is the number of occurrences of the pattern in t. Experimental results show that our method performs well in practice.
@article{265,
author = {J.W. Daykin, R. Groult, Y. Guesnet, T. Lecroq, A. Lefebvre, M. Leonard, L. Mouchard, E. Prieur-Gaston, Bruce Watson},
title = {Efficient pattern matching in degenerate strings with the Burrows–Wheeler transform},
abstract = {A degenerate or indeterminate string on an alphabet SIGMA is a sequence of non-empty subsets of SIGMA . Given a degenerate string t of length n and its Burrows–Wheeler transform we present a new method for searching for a degenerate pattern of length m in t running in O ( mn ) time on a constant size alphabet SIGMA. Furthermore, it is a hybrid pattern matching technique that works on both regular and degenerate strings. A degenerate string is said to be conservative if its number of non-solid letters is upper-bounded by a fixed positive constant q; in this case we show that the search time complexity is O ( qm^2 ) for counting
the number of occurrences and O ( qm^2 + occ ) for reporting the found occurrences where occ is the number of occurrences of the pattern in t. Experimental results show that our method performs well in practice.},
year = {2019},
journal = {Information Processing Letters},
volume = {147},
pages = {82 - 87},
publisher = {Elsevier},
doi = {https://doi.org/10.1016/j.ipl.2019.03.003},
}
1.
Runge T, Schaefer I, Knuppel A, Cleophas L, Kourie D, Watson B. Tool Support for Confidentiality-by-Construction. Ada User Journal . 2019;38(2). doi:https://doi.org/10.1145/3375408.3375413.
In many software applications, it is necessary to preserve confidentiality of information. Therefore, security mechanisms are needed to enforce that secret information does not leak to unauthorized users. However, most language-based techniques that enable in- formation flow control work post-hoc, deciding whether a specific program violates a confidentiality policy. In contrast, we proposed in previous work a refinement-based approach to derive programs that preserve confidentiality-by-construction. This approach follows the principles of Dijkstra’s correctness-by-construction. In this extended abstract, we present the implementation and tool support of that refinement-based approach allowing to specify the information flow policies first and to create programs in a simple while language which comply to these policies by construction. In particular, we present the idea of confidentiality-by-construction using an example and discuss the IDE C-CorC supporting this development approach.
@article{263,
author = {T. Runge, I. Schaefer, A. Knuppel, L.G.W.A. Cleophas, D.G Kourie, Bruce Watson},
title = {Tool Support for Confidentiality-by-Construction},
abstract = {In many software applications, it is necessary to preserve confidentiality of information. Therefore, security mechanisms are needed to enforce that secret information does not leak to unauthorized users. However, most language-based techniques that enable in- formation flow control work post-hoc, deciding whether a specific program violates a confidentiality policy. In contrast, we proposed in previous work a refinement-based approach to derive programs that preserve confidentiality-by-construction. This approach follows the principles of Dijkstra’s correctness-by-construction. In this extended abstract, we present the implementation and tool support of that refinement-based approach allowing to specify the information flow policies first and to create programs in a simple while language which comply to these policies by construction. In particular, we present the idea of confidentiality-by-construction using an example and discuss the IDE C-CorC supporting this development approach.},
year = {2019},
journal = {Ada User Journal},
volume = {38},
pages = {64 - 68},
issue = {2},
doi = {https://doi.org/10.1145/3375408.3375413},
}
1.
Runge T, Schaefer I, Cleophas L, Thum T, Kourie D, Watson B. Tool Support for Correctness-by-Construction. In: European Joint Conferences on Theory and Practice of Software (ETAPS). Switzerland: Springer; 2019. doi:https://doi.org/10.1007/978-3-030-16722-6 _ 2.
Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.
@{262,
author = {T. Runge, I. Schaefer, L.G.W.A. Cleophas, T. Thum, D.G Kourie, Bruce Watson},
title = {Tool Support for Correctness-by-Construction},
abstract = {Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.},
year = {2019},
journal = {European Joint Conferences on Theory and Practice of Software (ETAPS)},
pages = {25 - 42},
month = {06/04 - 11/04},
publisher = {Springer},
address = {Switzerland},
isbn = {78-3-030-16721-9},
url = {https://link.springer.com/content/pdf/10.1007/978-3-030-16722-6.pdf},
doi = {https://doi.org/10.1007/978-3-030-16722-6 _ 2},
}
1.
Watson B. The impact of using a contract-driven, test-interceptor based software development approach. In: Annual conference of The South African Institute of Computer Scientists and Information Technologists (SAICSIT 2018). New York: ACM; 2018. https://doi.org/10.475/123_4.
A contract-driven development approach requires the formalization of component requirements in the form of a component contract. The Use Case, Responsibility Driven Analysis and Design (URDAD) methodology is based on the contract-driven development approach and uses contracts to capture user requirements and perform a technology-neutral design across layers of granularity. This is achieved by taking use-case based functional requirements through an iterative design process and generating various levels of granularity iteratively.
In this project, the component contracts that were captured by utilizing the URDAD approach are used to generate test interceptors which validate whether, in the context of rendering component services, the component contracts are satisfied. To achieve this, Java classes and interfaces are annotated with pre- and postconditions to represent the contracts in code. Annotation processors are then used to automatically generate test-interceptor classes by processing the annotations. The test-interceptor classes encapsulate test-logic and are interface-compatible with their underlying component counterparts. This enable test-interceptors to intercept service requests to the underlying counterpart components in order to verify contract adherence. The generated test interceptors can be used for unit testing as well as real-time component monitoring. This development approach, utilized within the URDAD methodology would then result in unit and integration tests across levels of granularity.
Empirical data from actual software development projects will be used to assess the impact of introducing such a development approach in real software development projects. In particular, the study assesses the impact on the quality attributes of the software development process, as well as the qualities of the software produced by the process.
Process qualities measured include development productivity (the rate at which software is produced), correctness (the rate at which the produced software meets the clients requirements) and the certifiability of the software development process (which certifiability requirements are fully or partially addressed by the URDAD development approach). Software qualities measured include reusability (empirical and qualitative), simplicity (the inverse of the complexity measure) and bug density (number of defects in a module).
The study aims to show conclusively how the approach impacts the creation of correct software which meets the client requirements, how productivity is affected and if the approach enhances or hinders certifiability. The study also aims to determine if testinterceptors
are a viable mechanism to produce high-quality tests that contribute to the creation of correct software. Furthermore, the study aims to determine if the software produced by applying this approach yield improved reusability or not, if the software becomes
more or less complex and if more or less bugs are induced.
@{211,
author = {Bruce Watson},
title = {The impact of using a contract-driven, test-interceptor based software development approach},
abstract = {A contract-driven development approach requires the formalization of component requirements in the form of a component contract. The Use Case, Responsibility Driven Analysis and Design (URDAD) methodology is based on the contract-driven development approach and uses contracts to capture user requirements and perform a technology-neutral design across layers of granularity. This is achieved by taking use-case based functional requirements through an iterative design process and generating various levels of granularity iteratively.
In this project, the component contracts that were captured by utilizing the URDAD approach are used to generate test interceptors which validate whether, in the context of rendering component services, the component contracts are satisfied. To achieve this, Java classes and interfaces are annotated with pre- and postconditions to represent the contracts in code. Annotation processors are then used to automatically generate test-interceptor classes by processing the annotations. The test-interceptor classes encapsulate test-logic and are interface-compatible with their underlying component counterparts. This enable test-interceptors to intercept service requests to the underlying counterpart components in order to verify contract adherence. The generated test interceptors can be used for unit testing as well as real-time component monitoring. This development approach, utilized within the URDAD methodology would then result in unit and integration tests across levels of granularity.
Empirical data from actual software development projects will be used to assess the impact of introducing such a development approach in real software development projects. In particular, the study assesses the impact on the quality attributes of the software development process, as well as the qualities of the software produced by the process.
Process qualities measured include development productivity (the rate at which software is produced), correctness (the rate at which the produced software meets the clients requirements) and the certifiability of the software development process (which certifiability requirements are fully or partially addressed by the URDAD development approach). Software qualities measured include reusability (empirical and qualitative), simplicity (the inverse of the complexity measure) and bug density (number of defects in a module).
The study aims to show conclusively how the approach impacts the creation of correct software which meets the client requirements, how productivity is affected and if the approach enhances or hinders certifiability. The study also aims to determine if testinterceptors
are a viable mechanism to produce high-quality tests that contribute to the creation of correct software. Furthermore, the study aims to determine if the software produced by applying this approach yield improved reusability or not, if the software becomes
more or less complex and if more or less bugs are induced.},
year = {2018},
journal = {Annual conference of The South African Institute of Computer Scientists and Information Technologists (SAICSIT 2018)},
pages = {322-326},
month = {26/09-28/09},
publisher = {ACM},
address = {New York},
isbn = {123-4567-24-567/08/06},
url = {https://doi.org/10.475/123_4},
}
1.
Watson B. Three Strategies for the Dead-Zone String Matching Algorithm. In: The Prague Stringology Conference. Prague, Czech Republic: Prague Stringology Club; 2018. http://www.stringology.org/.
No Abstract
@{210,
author = {Bruce Watson},
title = {Three Strategies for the Dead-Zone String Matching Algorithm},
abstract = {No Abstract},
year = {2018},
journal = {The Prague Stringology Conference},
pages = {117-128},
month = {27/08-28/08},
publisher = {Prague Stringology Club},
address = {Prague, Czech Republic},
isbn = {978-80-01-06484-9},
url = {http://www.stringology.org/},
}
Research Groups:
More Info
Latest Research Publications:
No Results
