@inproceedings{, author = {Beyene, Tewodros and C{\^{a}}rlan, Carmen}, title = {{CyberGSN}: A Semi-formal Language for Specifying Safety Cases}, booktitle = {Proceedings of the 51st Annual {IEEE/IFIP} International Conference on Dependable Systems and Networks Workshops ({DSN-W})}, publisher = {IEEE}, year = {2021}, month = jun, abstract = {The use of safety cases to explicitly present safety considerations and decisions is a common practice in the safety-critical domain. A safety case can be used to scrutinize the safety assessment approach used by practitioners internally, or as an input for the certification process for an external certifying authority. However, safety cases are still created manually to explicate the followed safety assessment and assurance measures. In addition, although safety cases may be created in a modular way by multiple entities, and it may be critical for each entity to digitally sign its part of the assurance for accountability, the common notations are not expressive enough to include the notion of entity. Especially in cyber-security applications, the notion of entity is very critical. In this paper, we propose a formal logic based language called CyberGSN, with an explicit notion of entity, that can be used for specifying safety cases and safety case patterns, enabling the automated creation and maintenance of safety cases.}, doi = {10.1109/DSN-W52860.2021.00021}, keywords = {Safety Case, Pattern, Entity, Decentralization, Model-based Systems Engineering, MbSE}, } @article{Shankar, author = {Beyene, Tewodros and Herrera, Christian and Nigam, Vivek}, title = {Verification of Ada Programs with AdaHorn}, journal = {Ada User Journal}, volume = {40}, number = {2}, pages = {103-108}, year = {2019}, abstract = {We propose AdaHorn , a model checker for verification of Ada programs with respect to correctness properties given as assertions. AdaHorn translates an Ada program together with its assertion into a set of Constrained Horn Clauses, and feeds it to a Horn constraints solver. We evaluate the performance of AdaHorn on a set of Ada programs inspired by C programs from the software verification competition (SV-COMP). Our experimental results show that AdaHorn outputs correct results in more cases than GNATProve, which is a widely used Ada verification framework.}, } @inproceedings{, author = {Beyene, Tewodros and Rue{\ss}, Harald}, title = {Evidential and Continuous Integration of Software Verification Tools}, booktitle = {Formal Methods}, publisher = {Springer International Publishing}, pages = {679-685}, year = {2018}, address = {Cham}, } @inproceedings{, author = {Beyene, Tewodros and Popeea, Corneliu and Rybalchenko, Andrey}, title = {Efficient CTL Verification via Horn Constraints Solving}, booktitle = {HCVS@ETAPS}, year = {2016}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Beyene, Tewodros and Rue{\ss}, Harald}, title = {Integrated Formal Methods for Constructing Assurance Cases}, booktitle = {Proceedings of the 2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)}, publisher = {IEEE}, pages = {221--228}, year = {2016}, abstract = {The use of formal methods in verification activities is well established in various dedicated safety standards. Deficits in the verification process may have a negative impact on the confidence of verification results. Safety standards promote the use of integrated formal methods when a single method cannot achieve the verification objective without specifying how. In this paper, we take on the problem of using outputs from integrated formal methods as evidence in assurance cases, which are used in certification of safety-critical systems. We first present two workflows that employ integrated formal methods - code review workflow and code coverage workflow - corresponding to two of the most important activities of the verification phase. Then, we show how each workflow and the outputs from its integrated formal methods can be used in creating an assurance argument. These assurance arguments offer evidence for undeveloped goals identified in previous works from the field.}, doi = {10.1109/ISSREW.2016.21}, keywords = {Model-based Systems Engineering, MbSE}, }