Publications

book

  1. Villafiorita, A. (2014). Introduction to Software Project Management. Auerbach Publications. Retrieved from http://www.spmbook.com [BibTeX] More information...

    Abstract

    @book{Villafiorita:2014aa,
      author = {Villafiorita, Adolfo},
      keywords = {book},
      month = mar,
      publisher = {Auerbach Publications},
      title = {Introduction to Software Project Management},
      url = {http://www.spmbook.com},
      year = {2014}
    }
    
  2. Bozzano, M., & Villafiorita, A. (2010). Design and Safety Assessment of Critical Systems - A formal methods perspective. CRC Press (Taylor and Francis). Retrieved from http://www.safety-critical.org [Abstract] [BibTeX] More information...

    Abstract

    {Safety-critical systems - namely systems whose failure may cause death or injury to people, harm to the environment, or economical loss - are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Traditionally, safety analysis techniques and procedures are used to identify risks and hazards, with the goal of eliminating, avoiding, or reducing the probability of failure. However, these techniques are often performed manually, hence they are a time-consuming activity itself vulnerable to human error, since they rely on the ability of the safety engineer to understand and to foresee system behavior. The growing complexity of safety-critical systems requires an adequate increase in the capability of safety engineers to assess system safety, encouraging the adoption of formal techniques. This book is an introduction to the area of design and verification of safety critical systems, with a focus on safety assessment using formal methods. After an introduction covering the fundamental concepts in the areas of safety and reliability, the book illustrates the issues related to the design, development, and safety assessment of critical systems. The core of the book covers some of the most well-known notations, techniques, and procedures, and explains in detail how formal methods can be used to realize such procedures. Traditional verification and validation techniques and new trends in formal methods for safety assessment are described. The books ends with a discussion on the role of formal methods in the certification process. The book provides an in-depth and hands-on view on the application of formal techniques, that are applicable to a variety of industrial sectors, such as transportation, avionics and aerospace, and nuclear power.}
    @book{Bozzano:2010ly,
      abstract = {Safety-critical systems - namely systems whose failure may cause death or injury to people, harm to the environment, or economical loss - are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Traditionally, safety analysis techniques and procedures are used to identify risks and hazards, with the goal of eliminating, avoiding, or reducing the probability of failure. However, these techniques are often performed manually, hence they are a time-consuming activity itself vulnerable to human error, since they rely on the ability of the safety engineer to understand and to foresee system behavior. The growing complexity of safety-critical systems requires an adequate increase in the capability of safety engineers to assess system safety, encouraging the adoption of formal techniques.  This book is an introduction to the area of design and verification of safety critical systems, with a focus on safety assessment using formal methods. After an introduction covering the fundamental concepts in the areas of safety and reliability, the book illustrates the issues related to the design, development, and safety assessment of critical systems. The core of the book covers some of the most well-known notations, techniques, and procedures, and explains in detail how formal methods can be used to realize such procedures. Traditional verification and validation techniques and new trends in formal methods for safety assessment are described. The books ends with a discussion on the role of formal methods in the certification process. The book provides an in-depth and hands-on view on the application of formal techniques, that are applicable to a variety of industrial sectors, such as transportation, avionics and aerospace, and nuclear power.},
      author = {Bozzano, Marco and Villafiorita, Adolfo},
      keywords = {book},
      publisher = {CRC Press (Taylor and Francis)},
      title = {Design and Safety Assessment of Critical Systems - A formal methods perspective},
      topics = {safety_analysis, formal_methods, safety_critical_systems},
      url = {http://www.safety-critical.org},
      year = {2010}
    }
    

editor

  1. Costa, P., Ferlan, C., & Villafiorita, A. (Eds.). (2013). Chi Porta da Mangiare? Il Cibo tra eccessi e scarsità. FBK Press. Retrieved from https://books.fbk.eu/pubblicazioni/titoli/chi-porta-da-mangiare-il-cibo-tra-eccessi-e-scarsita/ [BibTeX] More information...

    Abstract

    @book{:2013aa,
      editor = {Costa, Paolo and Ferlan, Claudio and Villafiorita, Adolfo},
      keywords = {editor},
      month = dec,
      publisher = {FBK Press},
      title = {Chi Porta da Mangiare? Il Cibo tra eccessi e scarsità},
      year = {2013},
      url = {https://books.fbk.eu/pubblicazioni/titoli/chi-porta-da-mangiare-il-cibo-tra-eccessi-e-scarsita/}
    }
    
  2. Popescu-Zeletin, R., Jonas, K., Rai, I. A., Glitho, R., & Villafiorita, A. (Eds.). (2012). E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24 (Vol. 92). Springer. [Abstract] [BibTeX]

    Abstract

    {This book constitutes the thoroughly refereed post-conference proceedings of the Third International ICST Conference on e-Infrastructure and e-Services for Developing Countries, AFRICOMM 2011, held in Zanzibar, Tansania, in November 2011. The 24 revised full papers presented together with 2 poster papers were carefully reviewed and selected from numerous submissions. The papers cover a wide range of topics in the field of information and communication infrastructures. They are organized in two tracks: communication infrastructures for developing countries and electronic services, ICT policy, and regulatory issues for developing countries.}
    @proceedings{africomm-2011,
      abstract = {This book constitutes the thoroughly refereed post-conference proceedings of the Third International ICST Conference on e-Infrastructure and e-Services for Developing Countries, AFRICOMM 2011, held in Zanzibar, Tansania, in November 2011. The 24 revised full papers presented together with 2 poster papers were carefully reviewed and selected from numerous submissions. The papers cover a wide range of topics in the field of information and communication infrastructures. They are organized in two tracks: communication infrastructures for developing countries and electronic services, ICT policy, and regulatory issues for developing countries.},
      editor = {Popescu-Zeletin, Radu and Jonas, Karl and Rai, Idris A. and Glitho, R. and Villafiorita, Adolfo},
      keywords = {editor},
      month = apr,
      organization = {LNICST},
      publisher = {Springer},
      title = {E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24},
      topics = {ict4g},
      volume = {92},
      year = {2012}
    }
    
  3. Popescu-Zeletin, R., Rai, I. A., Jonas, K., & Villafiorita, A. (Eds.). (2011). E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa. Springer. [BibTeX]

    Abstract

    @proceedings{africomm-2010,
      editor = {Popescu-Zeletin, Radu and Rai, Idris A. and Jonas, Karl and Villafiorita, Adolfo},
      keywords = {editor},
      month = oct,
      organization = {LNICST},
      publisher = {Springer},
      title = {E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa},
      topics = {ict4g},
      year = {2011}
    }
    
  4. Villafiorita, A., Regis, S.-P., & Zorer, A. (Eds.). (2010). E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM December 2009, Maputo, Mozambique (Vol. 38). Springer. [BibTeX]

    Abstract

    @proceedings{africomm-2009,
      editor = {Villafiorita, Adolfo and Regis, Saint-Paul and Zorer, Alessandro},
      keywords = {editor},
      month = jun,
      organization = {LNICST},
      publisher = {Springer},
      title = {E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM December 2009, Maputo, Mozambique},
      topics = {ict4g},
      volume = {38},
      year = {2010}
    }
    

book_chapter

  1. Al-Shammari, A. F. N., & Villafiorita, A. (2014). A Synthesis of Vote Verification Methods in Electronic Voting Systems. In Design, Development, and Use of Secure Electronic Voting Systems. IGI Global. Retrieved from http://www.igi-global.com/book/design-development-use-secure-electronic/94868 [BibTeX] More information...

    Abstract

    @incollection{Al-Shammari2014A,
      author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo},
      booktitle = {Design, Development, and Use of Secure Electronic Voting Systems},
      keywords = {book_chapter},
      publisher = {IGI Global},
      title = {A Synthesis of Vote Verification Methods in Electronic Voting Systems},
      year = {2014},
      url = {http://www.igi-global.com/book/design-development-use-secure-electronic/94868}
    }
    
  2. Weldemariam, K., & Villafiorita, A. (2012). Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help? In M. Gupta, J. Walp, & R. Sharman (Eds.), Threats, Countermeasures, and Advances in Applied Information Security (pp. 361–380). IGI. [BibTeX]

    Abstract

    @incollection{WelVil12,
      author = {Weldemariam, Komminist and Villafiorita, Adolfo},
      booktitle = {Threats, Countermeasures, and Advances in Applied Information Security},
      editor = {Gupta, M. and Walp, J. and Sharman, R.},
      keywords = {book_chapter},
      pages = {361-380},
      publisher = {IGI},
      title = {Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help?},
      topics = {evoting, formal_methods, security},
      year = {2012}
    }
    
  3. Bozzano, M., & Villafiorita, A. (2012). Safety Critical Systems. In Encyclopedia of Software Engineering. CRC Press, Taylor & Francis Group. [Abstract] [BibTeX]

    Abstract

    {Safety critical systems—namely systems on which human lives depend—have to remain functional not only in nominal conditions, that is, when everything works as expected, but also when some of their components do not behave as expected. The methodologies, activities, and techniques to tackle this engineering challenge go under the name of safety analysis. This entry is an introduction to the development of safety critical systems with emphasis on some emerging techniques to support automated analysis and verification of complex systems.}
    @incollection{BozVil12,
      abstract = {Safety critical systems—namely systems on which human lives depend—have to remain functional not only in nominal conditions, that is, when everything works as expected, but also when some of their components do not behave as expected. The methodologies, activities, and techniques to tackle this engineering challenge go under the name of safety analysis. This entry is an introduction to the development of safety critical systems with emphasis on some emerging techniques to support automated analysis and verification of complex systems.},
      author = {Bozzano, Marco and Villafiorita, Adolfo},
      booktitle = {Encyclopedia of Software Engineering},
      keywords = {book_chapter},
      publisher = {CRC Press, Taylor & Francis Group},
      title = {Safety Critical Systems},
      topics = {safety_analysis, safety_critical_systems, standards},
      year = {2012}
    }
    
  4. Ciaghi, A., & Villafiorita, A. (2012). Law Modeling and BPR for Public Administration Improvement. In Handbook of Research on E-Government in Emerging Economies: Adoption, E-Participation, and Legal Frameworks (pp. 391–410). IGI. Retrieved from http://ict4g.net/adolfo/downloads/papers/law_modeling_and_bpr-2012.pdf [Abstract] [BibTeX] Download PDF...

    Abstract

    {ICTs are becoming more present in Public Administrations and in legal knowledge management. In most countries it is now possible for citizens to freely access the text of acts, bills, judgments, etc. Analysts that work on re-engineering Public Administration processes must take into account all relevant sources of law as they will ultimately be modified in order to legitimize the new processes. In this chapter, we consider the requirements to design a framework for Business Process Re-Engineering for Public Administrations by analyzing the existing systems for legal knowledge representation and interchange and the current technologies to assist modeling and change management of Business Processes. The ultimate goal is that of supporting the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations, by providing effective means to comprehend the law, make changes to the law and keep track of the dependencies between the text and the models.}
    @incollection{Ciaghi:2011kx,
      abstract = {ICTs are becoming more present in Public Administrations and in legal knowledge management. In most countries it is now possible for citizens to freely access the text of acts, bills, judgments, etc. Analysts that work on re-engineering Public Administration processes must take into account all relevant sources of law as they will ultimately be modified in order to legitimize the new processes. In this chapter, we consider the requirements to design a framework for Business Process Re-Engineering for Public Administrations by analyzing the existing systems for legal knowledge representation and interchange and the current technologies to assist modeling and change management of Business Processes. The ultimate goal is that of supporting the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations, by providing effective means to comprehend the law, make changes to the law and keep track of the dependencies between the text and the models.},
      author = {Ciaghi, Aaron and Villafiorita, Adolfo},
      booktitle = {Handbook of Research on E-Government in Emerging Economies: Adoption, E-Participation, and Legal Frameworks},
      keywords = {book_chapter},
      month = mar,
      pages = {391-410},
      publisher = {IGI},
      title = {Law Modeling and BPR for Public Administration Improvement},
      topics = {ict4laws, business_process_reengineering},
      url = {http://ict4g.net/adolfo/downloads/papers/law_modeling_and_bpr-2012.pdf},
      year = {2012}
    }
    
  5. Weldemariam, K., & Villafiorita, A. (2012). Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help? In M. Gupta, J. Walp, & R. Sharman (Eds.), Strategic and Practical Approaches for Information Security Governance: Technologies and Applied Solutions. IGI. [Abstract] [BibTeX]

    Abstract

    {In this chapter, first we discuss the current trends in the usage of formal techniques in the development of e-voting system. We then present our experiences on their usage to specify and verify the behaviors of one of currently deployed e-voting systems using formal techniques and verification against a subset of critical security properties that the system should meet. We also specified attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what we called the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where we would use formal techniques to improve the current development of e-voting systems. }
    @incollection{Weldemariam:2011fk,
      abstract = {In this chapter, first we discuss the current trends in the usage of formal techniques in the development of e-voting system. We then present our experiences on their usage to specify and verify the behaviors of one of currently deployed e-voting systems using formal techniques and verification against a subset of critical security properties that the system should meet. We also specified attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what we called the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where we would use formal techniques to improve the current development of e-voting systems.  },
      author = {Weldemariam, Komminist and Villafiorita, Adolfo},
      booktitle = {Strategic and Practical Approaches for Information Security Governance: Technologies and Applied Solutions},
      editor = {Gupta, Manish and Walp, John and Sharman, Raj},
      keywords = {book_chapter},
      month = feb,
      publisher = {IGI},
      title = {Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help?},
      topics = {formal_methods, evoting},
      year = {2012}
    }
    
  6. Cernuzzi, L., Gonzalez Magalı́, Ronchetti, M., Villafiorita, A., & Weldemariam, K. (2011). Multi-cultural experiences in eGovernance: Case Studies and a Roadmap. In W. C. Danilo Piagessi Kristian Sund (Ed.), Global Strategy and Practice of e-Governance: Examples from Around the World. IGI. Retrieved from http://www.igi-global.com/book/global-strategy-practice-governance/46168 [Abstract] [BibTeX] More information...

    Abstract

    {In a world characterized by rapid change driven by globalization, an ICT-based economy transformation poses some challenges and opportunities for the private sector and the government sector alike. ICT has for some time been at the core of government tasks, inseparable from strategy, planning, consultation and implementation to improve citizen‘s life in different ways. Nevertheless, indications are that the government sector has been falling behind in these practices (mostly in developing countries), compared to the private sector. This realization has prompted some governments to put ICT high on their policy agendas, with the aim of introducing ICT-based solutions to improve their public administration processes, and thus deliver "quality public services". We define ICT for Good (ICT4G) as the use of ICT to addressing critical problems in societies characterized by low ICT penetration in a way that life is impacted for the better. Along this line, we have been working on the design, development, and evaluation of ICT solutions that directly require the involvement of citizen on the usage of the developed system itself and/or on the decision-making processes. In this chapter, we discuss our experiences and lessons learned in this holistic approach to e-Governance projects from the ICT4G perspective and the role it can play for developing countries.}
    @incollection{Cernuzzi:2010ve,
      abstract = {In a world characterized by rapid change driven by globalization, an ICT-based economy transformation poses some challenges and opportunities for the private sector and the government sector alike. ICT has for some time been at the core of government tasks, inseparable from strategy, planning, consultation and implementation to improve citizen‘s life in different ways. Nevertheless, indications are that the government sector has been falling behind in these practices (mostly in developing countries), compared to the private sector. This realization has prompted some governments to put ICT high on their policy agendas, with the aim of introducing ICT-based solutions to improve their public administration processes, and thus deliver "quality public services". We define ICT for Good (ICT4G) as the use of ICT to addressing critical problems in societies characterized by low ICT penetration in a way that life is impacted for the better. Along this line, we have been working on the design, development, and evaluation of ICT solutions that directly require the involvement of citizen on the usage of the developed system itself and/or on the decision-making processes. In this chapter, we discuss our experiences and lessons learned in this holistic approach to e-Governance projects from the ICT4G perspective and the role it can play for developing countries.},
      author = {Cernuzzi, Luca and Gonzalez, Magalı́ and Ronchetti, Marco and Villafiorita, Adolfo and Weldemariam, Komminist},
      booktitle = {Global Strategy and Practice of e-Governance: Examples from Around the World},
      editor = {Danilo Piagessi, Kristian Sund, Walter Castelnovo},
      keywords = {book_chapter},
      publisher = {IGI},
      title = {Multi-cultural experiences in eGovernance: Case Studies and a Roadmap},
      topics = {egovernment, interoperability, ict4g},
      url = {http://www.igi-global.com/book/global-strategy-practice-governance/46168},
      year = {2011}
    }
    
  7. Shvaiko, P., Villafiorita, A., Zorer, A., Chemane, L., & Fumo, T. (2010). eGovernment Interoperability Framework: a case Study in a Developing Country. In C. G. Reddick (Ed.), Comparative E-Government (1st ed., Vol. 25). Springer. Retrieved from http://www.springer.com/it/book/9781441965356 [Abstract] [BibTeX] More information...

    Abstract

    {Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of resources, is a complex technical and organizational challenge. The problem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. The focus of the paper is on formulation of eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term.}
    @incollection{Shvaiko:2010zr,
      abstract = {Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of resources, is a complex technical and organizational challenge. The problem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. The focus of the paper is on formulation of eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term.},
      author = {Shvaiko, Pavel and Villafiorita, Adolfo and Zorer, Alessandro and Chemane, Lourino and Fumo, Teotónio},
      booktitle = {Comparative E-Government},
      edition = {1st},
      editor = {Reddick, Christopher G},
      isbn = {978-1-4419-6535-6},
      keywords = {book_chapter},
      publisher = {Springer},
      series = {Integrated Series in Information Systems},
      tags = {egif4m-2010.pdf},
      title = {eGovernment Interoperability Framework: a case Study in a Developing Country},
      topics = {egovernment, interoperability, ict4g},
      url = {http://www.springer.com/it/book/9781441965356},
      volume = {25},
      year = {2010}
    }
    

journal

  1. Grau, I., Travassos, G. H., Cernuzzi, L., & Villafiorita, A. (2015). Tape Mbo’e: A First Experimental Assessment. CLEI Electronic Journal, 18, CIbSE 2014 Special Issue(1), 26. Retrieved from http://www.clei.org/cleiej/paper.php?id=328 [Abstract] [BibTeX] More information...

    Abstract

    {The development of software not only needs to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions, such as service oriented architecture, must be considered as the basic style to build sustainable applications into environments were practitioners are not aware of this software technology. In addition to this, most of the available software processes are not directly applicable nor are they reusable, so learning times becomes risk for the development of the project. Therefore, Tape Mbo´e (TME) has been proposed to support the building of such applications, into development environments like developing countries where we can have economic constraints and scarcity of proficient practitioners. The first application of TME has been to develop a service-based application whose goal is to provide the interoperability among legacy systems of different public agencies in Paraguay. Initial results of this experience indicated the feasibility and simplicity of TME when applied in this field. The evaluation process, its results and conclusions are described in this paper. }
    @article{Grau:2015aa,
      abstract = {The development of software not only needs to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions, such as service oriented architecture, must be considered as the basic style to build sustainable applications into environments were practitioners are not aware of this software technology. In addition to this, most of the available software processes are not directly applicable nor are they reusable, so learning times becomes risk for the development of the project. Therefore, Tape Mbo´e (TME) has been proposed to support the building of such applications, into development environments like developing countries where we can have economic constraints and scarcity of proficient practitioners.  The first application of TME has been to develop a service-based application whose goal is to provide the interoperability among legacy systems of different public agencies in Paraguay. Initial results of this experience indicated the feasibility and simplicity of TME when applied in this field. The evaluation process, its results and conclusions are described in this paper. },
      author = {Grau, Ilse and Travassos, Guilherme H. and Cernuzzi, Luca and Villafiorita, Adolfo},
      journal = {CLEI electronic journal},
      keywords = {journal},
      month = apr,
      number = {1},
      pages = {26},
      title = {Tape Mbo’e: A First Experimental Assessment},
      url = {http://www.clei.org/cleiej/paper.php?id=328},
      volume = {18, CIbSE 2014 Special Issue},
      year = {2015}
    }
    
  2. Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2011). Formal analysis of an electronic voting system: An experience report. Journal of Systems and Software, 84(10), 1618–1637. [Abstract] [BibTeX]

    Abstract

    {We have seen that several currently deployed e-voting systems share critical failures in their design and implementation that render their technical and procedural controls insufficient to guarantee trustworthy voting. The application of formal methods would greatly help to better address problems associated with assurance against requirements and standards. More specifically, it would help to thoroughly specify and analyze the underlying assumptions and security specific properties, and it would improve the trustworthiness of the final systems. In this article, we show how such techniques can be used to model and reason about the security of one of the currently deployed e-voting systems in the U.S.A named ES&S. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. We also believe that besides analyzing the system against its requirements, it is equally important to perform an analysis under malicious circumstances where the execution model is augmented with attack behaviors. Thus, we extend the formal specification of the system by specifying attacks that have been shown to successfully compromise the system, and we then repeat the formal verification. This is helpful in detecting missing requirements or unwarranted assumptions about the specification of the system. In addition, this allows one to sketch countermeasure strategies to be used when the system behaves differently than it should and to build confidence about the system under development. Finally, we acknowledge the main problem that arises in e-voting system specification and verification: modeling attacks is very difficult because the different types of attack often cut across the structure of the original behavior models, thus making (incremental or compositional) verification very difficult.}
    @article{Weldemariam20111618,
      abstract = {We have seen that several currently deployed e-voting systems share critical failures in their design and implementation that render their technical and procedural controls insufficient to guarantee trustworthy voting. The application of formal methods would greatly help to better address problems associated with assurance against requirements and standards. More specifically, it would help to thoroughly specify and analyze the underlying assumptions and security specific properties, and it would improve the trustworthiness of the final systems. In this article, we show how such techniques can be used to model and reason about the security of one of the currently deployed e-voting systems in the U.S.A named ES&S. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. We also believe that besides analyzing the system against its requirements, it is equally important to perform an analysis under malicious circumstances where the execution model is augmented with attack behaviors. Thus, we extend the formal specification of the system by specifying attacks that have been shown to successfully compromise the system, and we then repeat the formal verification. This is helpful in detecting missing requirements or unwarranted assumptions about the specification of the system. In addition, this allows one to sketch countermeasure strategies to be used when the system behaves differently than it should and to build confidence about the system under development. Finally, we acknowledge the main problem that arises in e-voting system specification and verification: modeling attacks is very difficult because the different types of attack often cut across the structure of the original behavior models, thus making (incremental or compositional) verification very difficult.},
      author = {Weldemariam, Komminist and Kemmerer, Richard A. and Villafiorita, Adolfo},
      journal = {Journal of Systems and Software},
      keywords = {journal},
      number = {10},
      pages = {1618-1637},
      title = {Formal analysis of an electronic voting system: An experience report},
      topics = {evoting, formal_methods},
      volume = {84},
      year = {2011}
    }
    
  3. Weldemariam, K., & Villafiorita, A. (2011). Procedural Security Analysis: A Methodological Approach. Journal of Systems and Software, 84(7), 1114–1129. http://doi.org/10.1016/j.jss.2011.01.064 [Abstract] [BibTeX]

    Abstract

    {This article introduces what we call procedural security analysis, an approach that allows for a systematic security assessment of (business) processes. The approach is based on explicit reasoning on asset flows and is implemented by building formal models to describe the nominal procedures under analysis, by injecting possible threat-actions of such models, and by assuming that any combination of threats can be possible in all steps into such models. We use the NuSMV input language to encode the asset flows, which are amenable for formal analysis. This allows us to understand how the switch to a new techno- logical solution changes the requirements of an organization, with the ultimate goal of defining the new processes that ensure a sufficient level of security. We have applied the technique to a real-world electronic voting system named ProVotE to analyze the procedures used during and after elections. Such analyses are essential to identify the limits of the current procedures (i.e., conditions under which attacks are undetectable) and to identify the hypotheses that can guarantee reasonably secure electronic elections. Additionally, the results of the analyses can be a step forward to devise a set of requirements, to be applied both at the organizational level and on the (software) systems to make them more secure.}
    @article{Weldemariam:2011yq,
      abstract = {This article introduces what we call procedural security analysis, an approach that allows for a systematic security assessment of (business) processes. The approach is based on explicit reasoning on asset flows and is implemented by building formal models to describe the nominal procedures under analysis, by injecting possible threat-actions of such models, and by assuming that any combination of threats can be possible in all steps into such models. We use the NuSMV input language to encode the asset flows, which are amenable for formal analysis. This allows us to understand how the switch to a new techno- logical solution changes the requirements of an organization, with the ultimate goal of defining the new processes that ensure a sufficient level of security.  We have applied the technique to a real-world electronic voting system named ProVotE to analyze the procedures used during and after elections. Such analyses are essential to identify the limits of the current procedures (i.e., conditions under which attacks are undetectable) and to identify the hypotheses that can guarantee reasonably secure electronic elections. Additionally, the results of the analyses can be a step forward to devise a set of requirements, to be applied both at the organizational level and on the (software) systems to make them more secure.},
      author = {Weldemariam, Komminist and Villafiorita, Adolfo},
      doi = {10.1016/j.jss.2011.01.064},
      journal = {Journal of Systems and Software},
      keywords = {journal},
      month = jul,
      number = {7},
      pages = {1114-1129},
      title = {Procedural Security Analysis: A Methodological Approach},
      topics = {procedural_security_analysis, evoting},
      volume = {84},
      year = {2011}
    }
    
  4. Weldemariam, K., Siena, A., Villafiorita, A., & Susi, A. (2011). Enhancing Law Modeling and Analysis: using BPR-Based and Goal-Oriented Frameworks. International Journal on Advances in Security, 3(3-4), 80–90. [Abstract] [BibTeX]

    Abstract

    {In recent years, new laws have been enacted to explicitly regulate sensitive matters such as business and health assistance, when, for example, performed on networked systems. Existing laws have been revised and also gained new meaning when referred to an Internet-based activity. As a result of this, concerns like security, privacy and governance are increasingly the focus of (digital) government regulations around the world. This trend has created a challenge in the definition and/or redesign of Public Administration (PA) processes. This trend has also created a challenge in the compliance of regulations, whereby PA officers, lawmakers, software engineers are required to ensure that their software delivery complies with relevant regulations, either through design or reengineering activity. Previously we proposed two complementary frameworks — the Nomos and VLPM frameworks — to systematically model and analyze laws. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal realization for the requirements guided by the satisfiability of normative proposition(s) obtained from rules embedded in the law. VLPM, whereas is a tool-supported BPR methodology to extract laws represented in XML and build models using a subset of UML diagrams. In this paper1, we provide detailed overview of the two frameworks and their integration whose aim is to improve the current modeling and analysis of laws by providing a uniform environment that can be used both at modeling time and for laws assessment. The integration of process and goal-oriented ontologies with the VLPM framework would also make easier the modeling and analysis of laws and procedures and provide a facility for interchanging models among the tools. We believe that, this provides a framework that allows tracing and reasoning either top-down, from the principles to the implementation or, vice versa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than the simple juxtaposition of the two techniques. Finally, we use an example to examine the combined offer.}
    @article{Weldemariam:2011kx,
      abstract = {In recent years, new laws have been enacted to explicitly regulate sensitive matters such as business and health assistance, when, for example, performed on networked systems. Existing laws have been revised and also gained new meaning when referred to an Internet-based activity. As a result of this, concerns like security, privacy and governance are increasingly the focus of (digital) government regulations around the world. This trend has created a challenge in the definition and/or redesign of Public Administration (PA) processes. This trend has also created a challenge in the compliance of regulations, whereby PA officers, lawmakers, software engineers are required to ensure that their software delivery complies with relevant regulations, either through design or reengineering activity.  Previously we proposed two complementary frameworks — the Nomos and VLPM frameworks — to systematically model and analyze laws. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal realization for the requirements guided by the satisfiability of normative proposition(s) obtained from rules embedded in the law. VLPM, whereas is a tool-supported BPR methodology to extract laws represented in XML and build models using a subset of UML diagrams.  In this paper1, we provide detailed overview of the two frameworks and their integration whose aim is to improve the current modeling and analysis of laws by providing a uniform environment that can be used both at modeling time and for laws assessment. The integration of process and goal-oriented ontologies with the VLPM framework would also make easier the modeling and analysis of laws and procedures and provide a facility for interchanging models among the tools. We believe that, this provides a framework that allows tracing and reasoning either top-down, from the principles to the implementation or, vice versa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than the simple juxtaposition of the two techniques. Finally, we use an example to examine the combined offer.},
      author = {Weldemariam, Komminist and Siena, Alberto and Villafiorita, Adolfo and Susi, Angelo},
      journal = {International Journal on Advances in Security},
      keywords = {journal},
      month = apr,
      number = {3-4},
      pages = {80-90},
      title = {Enhancing Law Modeling and Analysis: using BPR-Based and Goal-Oriented Frameworks},
      topics = {ict4laws, business_process_reengineering},
      volume = {3},
      year = {2011}
    }
    
  5. Bryl, V., Dalpiaz, F., Ferrario, R., Mattioli, A., & Villafiorita, A. (2009). Evaluating procedural alternatives: a case study in e-voting. Electronic Government, an International Journal, 6(2), 213–231. [Abstract] [BibTeX]

    Abstract

    {This paper describes part of the work within the ProVotE project, whose goal is the introduction of e-voting systems for local elections. The approach is aimed at providing both precise models of the electoral processes and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures. It is based on defining an alternating sequence of models, written using UML and Tropos. The UML is used to represent electoral processes (both existing and future), while Tropos provides a mean to reason and document the decisions taken about how to change the existing procedures to support an electronic election.}
    @article{Bryl:2009ys,
      abstract = {This paper describes part of the work within the ProVotE project, whose goal is the introduction of e-voting systems for local elections. The approach is aimed at providing both precise models of the electoral processes and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures. It is based on defining an alternating sequence of models, written using UML and Tropos. The UML is used to represent electoral processes (both existing and future), while Tropos provides a mean to reason and document the decisions taken about how to change the existing procedures to support an electronic election.},
      author = {Bryl, Volha and Dalpiaz, Fabiano and Ferrario, Roberta and Mattioli, Andrea and Villafiorita, Adolfo},
      journal = {Electronic Government, an International Journal},
      keywords = {journal},
      number = {2},
      pages = {213 - 231},
      title = {Evaluating procedural alternatives: a case study in e-voting},
      topics = {procedural_security_analysis, evoting, business_process_reenegineering},
      volume = {6},
      year = {2009}
    }
    
  6. Villafiorita, A., Weldemariam, K., & Tiella, R. (2009). Development, Formal Verification, and Evaluation of an E-Voting System With VVPAT. IEEE Transactions on Information Forensics and Security, 4(4 part 1), 651–661. [Abstract] [BibTeX]

    Abstract

    {The use of new technologies to support voting has been and is the subject of great debate. Several people advocate the benefits it can bring — such as improved speed and accuracy in counting, accessibility, voting from home — and as many are concerned with the risks it poses, such as unequal access (digital divide), violation to secrecy and anonymity, alteration of the results of an election (because of malicious attacks, bad design/coding, or procedural weaknesses). The attitude of different governments towards electronic voting (e-voting) varies accordingly. In this paper we present the activities related to the development and formal verification of an e-voting system, called ProVotE . ProVotE is an end-to-end e-voting system with Voter Verified Paper Audit Trial (VVPAT), developed within the framework of a larger initiative whose goal is assessing the feasibility of introducing e-voting in the Autonomous Province of Trento. ProVotE has been used in trials and elections with legal value in Italy. What we believe to be of interest is the approach we took for its development, which has been based on a participatory design for the definition of the voter interface, on the usage of formal methods and model checking for the validation of the core logic of the machine, on open source components, and on the formal analysis of some critical procedures related to the usage of the machine during the election.}
    @article{Villafiorita:2009vn,
      abstract = {The use of new technologies to support voting has been and is the subject of great debate. Several people advocate the benefits it can bring — such as improved speed and accuracy in counting, accessibility, voting from home — and as many are concerned with the risks it poses, such as unequal access (digital divide), violation to secrecy and anonymity, alteration of the results of an election (because of malicious attacks, bad design/coding, or procedural weaknesses). The attitude of different governments towards electronic voting (e-voting) varies accordingly. In this paper we present the activities related to the development and formal verification of an e-voting system, called ProVotE . ProVotE is an end-to-end e-voting system with Voter Verified Paper Audit Trial (VVPAT), developed within the framework of a larger initiative whose goal is assessing the feasibility of introducing e-voting in the Autonomous Province of Trento. ProVotE has been used in trials and elections with legal value in Italy. What we believe to be of interest is the approach we took for its development, which has been based on a participatory design for the definition of the voter interface, on the usage of formal methods and model checking for the validation of the core logic of the machine, on open source components, and on the formal analysis of some critical procedures related to the usage of the machine during the election.},
      author = {Villafiorita, Adolfo and Weldemariam, Komminist and Tiella, Roberto},
      journal = {IEEE Transactions on Information Forensics and Security},
      keywords = {journal},
      month = dec,
      number = {4 part 1},
      pages = {651-661},
      title = {Development, Formal Verification, and Evaluation of an E-Voting System With VVPAT},
      topics = {software_engineering_process, software_quality, evoting, formal_methods},
      volume = {4},
      year = {2009}
    }
    
  7. Bozzano, M., & Villafiorita, A. (2007). The FSAP/NuSMV-SA Safety Analysis Platform. International Journal on Software Tools for Technology Transfer, 9(1), 5–24. [Abstract] [BibTeX]

    Abstract

    {Safety-critical systems are becoming more com- plex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, in- cluding analyzing the behaviour of a system in degraded sit- uations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complex- ity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited. In this paper we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex sys- tems easier by providing a facility for automatically augment- ing a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, that is, in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements. The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been imple- mented to automate the generation of artifacts that are typi- cal of reliability analysis, for example fault trees. The plat- form can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the sys- tem model and of the possible faults. The interface of the platform has been designed to im- prove usability for people that are not expert in formal verifi- cation. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies.}
    @article{Bozzano:2007oz,
      abstract = {Safety-critical systems are becoming more com- plex, both in the type of functionality they provide and in the way they are demanded to interact with the environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, in- cluding analyzing the behaviour of a system in degraded sit- uations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complex- ity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited.  In this paper we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex sys- tems easier by providing a facility for automatically augment- ing a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, that is, in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements.  The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been imple- mented to automate the generation of artifacts that are typi- cal of reliability analysis, for example fault trees. The plat- form can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the sys- tem model and of the possible faults.  The interface of the platform has been designed to im- prove usability for people that are not expert in formal verifi- cation. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies.},
      author = {Bozzano, Marco and Villafiorita, Adolfo},
      journal = {International Journal on Software Tools for Technology Transfer},
      keywords = {journal},
      number = {1},
      pages = {5–24},
      publisher = {Springer},
      title = {The FSAP/NuSMV-SA Safety Analysis Platform},
      topics = {safety_analysis, formal_methods},
      volume = {9},
      year = {2007}
    }
    
  8. Bundy, A., Giunchiglia, F., Villafiorita, A., & Walsh, T. (1997). Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem. Journal of Automated Reasoning, 19(3), 319–346. [Abstract] [BibTeX]

    Abstract

    {We demonstrate the use of abstraction in aiding the construction of an interesting and difficult example in a proof checking system. This experiment demonstrates that abstraction can make proofs easier to comprehend and to verify mechanically. To support such proof checking, we have developed a formal theory of abstraction and added facilities for using abstraction to the GETFOL proof checking system.}
    @article{Bundy:1997pt,
      abstract = {We demonstrate the use of abstraction in aiding the construction of an interesting and difficult example in a proof checking system. This experiment demonstrates that abstraction can make proofs easier to comprehend and to verify mechanically. To support such proof checking, we have developed a formal theory of abstraction and added facilities for using abstraction to the GETFOL proof checking system.},
      author = {Bundy, Alan and Giunchiglia, Fausto and Villafiorita, Adolfo and Walsh, Toby},
      issn = {1573-0670},
      journal = {Journal of Automated Reasoning},
      keywords = {journal},
      number = {3},
      pages = {319–346},
      publisher = {Springer},
      title = {Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem},
      topics = {abstraction, goedel_incompleteness_theorem, theorem_proving},
      volume = {19},
      year = {1997}
    }
    
  9. Giunchiglia, F., Villafiorita, A., & Walsh, T. (1999). Theories of Abstraction. Ai Communications, 10(3-4), 167–176. [Abstract] [BibTeX]

    Abstract

    {In the past years, several different theories and frameworks for describing and using abstraction have been proposed. In this paper we overview several of the theories proposed in the past and we argue that each of these works is trying to capture the same intuitive idea, that is, that abstraction is the mapping from one representation of a problem to another which preserves certain desirable properties and which reduces complexity.}
    @article{Giunchiglia:1999xq,
      abstract = {In the past years, several different theories and frameworks for describing and using abstraction have been proposed. In this paper we overview several of the theories proposed in the past and we argue that each of these works is trying to capture the same intuitive idea, that is, that abstraction is the mapping from one representation of a problem to another which preserves certain desirable properties and which reduces complexity.},
      author = {Giunchiglia, Fausto and Villafiorita, Adolfo and Walsh, Toby},
      issn = {0921-7126},
      journal = {Ai Communications},
      keywords = {journal},
      number = {3-4},
      pages = {167–176},
      publisher = {IOS Press},
      title = {Theories of Abstraction},
      topics = {abstraction, theorem_proving},
      volume = {10},
      year = {1999}
    }
    
  10. Benerecetti, M., & Villafiorita, A. (1999). Formal specification of Beliefs in Multi-Agents Systems. International Journal of Intelligent Systems, 14(10), 1021–1040. [Abstract] [BibTeX]

    Abstract

    {The goal of this paper is to present a logical framework for the formalization of agents’ mutual beliefs in a Multi Agent system. The approach is based on a combination of exten- sional specifications of beliefs and context-based (finite) presentation of the specifications by employing a particular class of Multi Context systems. The extensional specification provides a set-theoretic characterization of beliefs in terms of sets closed under certain conditions. Its finite presentation is provided by using as constructors inference rules in- side a Multi Context system. The resulting framework allows for capturing many relevant cases of real (non omniscient) agents, which are very common in Multi Agent scenarios embedded in real world environments. In order to substantiate this claim, two Multi Agent scenarios are formally specified in detail in the specification framework.}
    @article{Benerecetti:1999qq,
      abstract = {The goal of this paper is to present a logical framework for the formalization of agents’ mutual beliefs in a Multi Agent system. The approach is based on a combination of exten- sional specifications of beliefs and context-based (finite) presentation of the specifications by employing a particular class of Multi Context systems. The extensional specification provides a set-theoretic characterization of beliefs in terms of sets closed under certain conditions. Its finite presentation is provided by using as constructors inference rules in- side a Multi Context system. The resulting framework allows for capturing many relevant cases of real (non omniscient) agents, which are very common in Multi Agent scenarios embedded in real world environments. In order to substantiate this claim, two Multi Agent scenarios are formally specified in detail in the specification framework.},
      author = {Benerecetti, Massimo and Villafiorita, Adolfo},
      journal = {International Journal of Intelligent Systems},
      keywords = {journal},
      note = {10.1002-int.20364.},
      number = {10},
      pages = {1021–1040},
      publisher = {Wiley},
      title = {Formal specification of Beliefs in Multi-Agents Systems},
      topics = {theorem_proving},
      volume = {14},
      year = {1999}
    }
    
  11. Ciaghi, A., Mattioli, A., & Villafiorita, A. (2010). A Tool Supported Methodology for BPR in Public Administrations. International Journal of Electronic Governance (IJEG), 3(2). Retrieved from http://www.inderscience.com/info/inarticle.php?artid=24443 [Abstract] [BibTeX] More information...

    Abstract

    {In Public Administration (PA), business process redesign is an essential activity for reducing costs, has strict connections with laws and is carried out by actors with different backgrounds. This work proposes an approach where changes in the law are mapped in process diagrams in order to highlight and review the impact on processes. This allows for a stricter collaboration among the different people usually involved in Business Process Reengineering (BPR). The methodology takes advantage of the UML notation and is supported by a tool, Visual Law Process Modeller (VLPM), which helps to keep traceability between processes and laws. Finally, we discuss an example in which the methodology was applied to model the transition from electoral processes to e-electoral process.}
    @article{Ciaghi:2010kn,
      abstract = {In Public Administration (PA), business process redesign is an essential activity for reducing costs, has strict connections with laws and is carried out by actors with different backgrounds. This work proposes an approach where changes in the law are mapped in process diagrams in order to highlight and review the impact on processes. This allows for a stricter collaboration among the different people usually involved in Business Process Reengineering (BPR). The methodology takes advantage of the UML notation and is supported by a tool, Visual Law Process Modeller (VLPM), which helps to keep traceability between processes and laws. Finally, we discuss an example in which the methodology was applied to model the transition from electoral processes to e-electoral process.},
      author = {Ciaghi, Aaron and Mattioli, Andrea and Villafiorita, Adolfo},
      journal = {International Journal of Electronic Governance (IJEG)},
      keywords = {journal},
      number = {2},
      publisher = {InderScience Publishers},
      title = {A Tool Supported Methodology for BPR in Public Administrations},
      topics = {business_process_reengineering, egovernment},
      url = {http://www.inderscience.com/info/inarticle.php?artid=24443},
      volume = {3},
      year = {2010}
    }
    

conference

  1. Grau, I., Cernuzzi, L., & Villafiorita, A. (2014). Analyzing Service Oriented Methodologies for Sustainable Applications. In XXXII International Conference of The Chilean Computer Science Society. [BibTeX]

    Abstract

    @conference{Grau:2014aa,
      author = {Grau, Ilse and Cernuzzi, Luca and Villafiorita, Adolfo},
      booktitle = {XXXII International Conference of The Chilean Computer Science Society},
      keywords = {conference},
      title = {Analyzing Service Oriented Methodologies for Sustainable Applications},
      year = {2014}
    }
    
  2. Al-Shammari, A. F. N., & Villafiorita, A. (2014). Iraqi Elections in 2014: a Privacy Requirement Evaluation Based on a Polling Place Experience. In Proceeding of INFORMATIK 2014, Big Data-Komplexitat meistern, Stuttgart, Germany (pp. 1359–1370). [BibTeX]

    Abstract

    @inproceedings{Al-Shammari2014,
      author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo},
      booktitle = {Proceeding of INFORMATIK 2014, Big Data-Komplexitat meistern, Stuttgart, Germany},
      keywords = {conference},
      pages = {1359-1370},
      title = {Iraqi Elections in 2014: a Privacy Requirement Evaluation Based on a Polling Place Experience},
      year = {2014}
    }
    
  3. Ciaghi, A., Molini, P., Villafiorita, A., & Weldemariam, K. S. (2013). Maputo living lab summer school of ICTs: An experience report. In IST-Africa Conference and Exhibition (IST-Africa), 2013 (pp. 1–8). [Abstract] [BibTeX]

    Abstract

    {This paper presents our experience with the organization of the Summer School of ICTs (SSICT) of Maputo Living Lab. SSICT is a free 1-month course for 3rd and 4th year undergraduate students that provides practical training on the management, design and development of software projects that can have an impact on the local society. The School has been organized for 2 editions in 2011 and 2012 in Maputo, Mozambique and it is part of the larger Maputo Living Lab project.}
    @inproceedings{6701783,
      abstract = {This paper presents our experience with the organization of the Summer School of ICTs (SSICT) of Maputo Living Lab. SSICT is a free 1-month course for 3rd and 4th year undergraduate students that provides practical training on the management, design and development of software projects that can have an impact on the local society. The School has been organized for 2 editions in 2011 and 2012 in Maputo, Mozambique and it is part of the larger Maputo Living Lab project.},
      author = {Ciaghi, A. and Molini, P. and Villafiorita, A. and Weldemariam, K.S.},
      booktitle = {IST-Africa Conference and Exhibition (IST-Africa), 2013},
      keywords = {conference},
      month = may,
      pages = {1-8},
      title = {Maputo living lab summer school of ICTs: An experience report},
      year = {2013}
    }
    
  4. 37th Annual IEEE Computer Software and Applications Conference, COMPSAC 2013, Kyoto, Japan, July 22-26, 2013. (2013). COMPSAC. IEEE Computer Society. [BibTeX]

    Abstract

    @proceedings{DBLP:conf/compsac/2013,
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {COMPSAC},
      isbn = {978-0-7695-4986-6},
      keywords = {conference},
      publisher = {IEEE Computer Society},
      title = {37th Annual IEEE Computer Software and Applications Conference, COMPSAC 2013, Kyoto, Japan, July 22-26, 2013},
      year = {2013}
    }
    
  5. Zewge, A., Weldemariam, K., Hailemariam, S., Villafiorita, A., Susi, A., & Belachew, M. (2012). On the use of goal-oriented methodology for designing agriculture services in developing countries. In Proceedings of the International Conference on Management of Emergent Digital EcoSystems (pp. 40–47). New York, NY, USA: ACM. http://doi.org/10.1145/2457276.2457285 [BibTeX] More information...

    Abstract

    @inproceedings{Zewge:2012:UGM:2457276.2457285,
      acmid = {2457285},
      address = {New York, NY, USA},
      author = {Zewge, Amanuel and Weldemariam, Komminist and Hailemariam, Sebsibe and Villafiorita, Adolfo and Susi, Angelo and Belachew, Mesfin},
      booktitle = {Proceedings of the International Conference on Management of Emergent Digital EcoSystems},
      doi = {10.1145/2457276.2457285},
      isbn = {978-1-4503-1755-9},
      keywords = {conference},
      location = {Addis Ababa, Ethiopia},
      numpages = {8},
      pages = {40–47},
      publisher = {ACM},
      series = {MEDES ’12},
      title = {On the use of goal-oriented methodology for designing agriculture services in developing countries},
      url = {http://dl.acm.org/citation.cfm?doid=2457276.2457285},
      year = {2012}
    }
    
  6. Al-Shammari, A. F. N., Villafiorita, A., & Weldemariam, K. (2012). Towards an Open Standard Vote Verification Framework in Electronic Voting Systems. In ARES (pp. 437–444). IEEE Computer Society. [BibTeX]

    Abstract

    @inproceedings{DBLP:conf/IEEEares/Al-ShammariVW12a,
      author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ARES},
      keywords = {conference},
      pages = {437-444},
      title = {Towards an Open Standard Vote Verification Framework in Electronic Voting Systems},
      year = {2012}
    }
    
  7. Al-Shammari, A. F. N., Villafiorita, A., & Weldemariam, K. (2012). Understanding the Development Trends of Electronic Voting Systems. In ARES (pp. 186–195). IEEE Computer Society. [BibTeX]

    Abstract

    @inproceedings{DBLP:conf/IEEEares/Al-ShammariVW12,
      author = {Al-Shammari, Ali Fawzi Najm and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ARES},
      keywords = {conference},
      pages = {186-195},
      title = {Understanding the Development Trends of Electronic Voting Systems},
      year = {2012}
    }
    
  8. Eshete, B., Villafiorita, A., & Weldemariam, K. (2012). BINSPECT: Holistic Analysis and Detection of Malicious Web Pages. In A. D. Keromytis & R. D. Pietro (Eds.), SecureComm (Vol. 106, pp. 149–166). Springer. [BibTeX]

    Abstract

    @inproceedings{DBLP:conf/securecomm/EsheteVW12,
      author = {Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {SecureComm},
      keywords = {conference},
      pages = {149-166},
      title = {BINSPECT: Holistic Analysis and Detection of Malicious Web Pages},
      year = {2012}
    }
    
  9. Eshete, B., Weldemariam, K., Villafiorita, A., & Zulkernine, M. (2013). Confeagle: Automated Analysis of Security Configuration Vulnerabilities in Web Applications. In In Proceedings of the International Conference on Security and Reliability (SERE). [BibTeX]

    Abstract

    @inproceedings{Eshete:2013aa,
      author = {Eshete, Birhanu and Weldemariam, Komminist and Villafiorita, Adolfo and Zulkernine, Mohammad},
      booktitle = {In Proceedings of the International Conference on Security and Reliability (SERE)},
      keywords = {conference},
      title = {Confeagle: Automated Analysis of Security Configuration Vulnerabilities in Web Applications},
      year = {2013}
    }
    
  10. Ciaghi, A., Molini, P., Villafiorita, A., & Weldemariam, K. (2013). Maputo Living Lab Summer School of ICTs: an Experience Report. In Accepted at IST-Africa 2013. [BibTeX]

    Abstract

    @inproceedings{Ciaghi:2013aa,
      author = {Ciaghi, Aaron and Molini, Pietro and Villafiorita, Adolfo and Weldemariam, Komminist},
      booktitle = {Accepted at IST-Africa 2013},
      keywords = {conference},
      title = {Maputo Living Lab Summer School of ICTs: an Experience Report},
      year = {2013}
    }
    
  11. Ciaghi, A., Eshete, B., Molini, P., & Villafiorita, A. (2013). SAMo: Experimenting a Social Accountability Web Platform. In B. Thies & A. Nanavati (Eds.), ACM DEV (p. 17). ACM. [BibTeX]

    Abstract

    @inproceedings{DBLP:conf/dev/CiaghiEMV13,
      author = {Ciaghi, Aaron and Eshete, Birhanu and Molini, Pietro and Villafiorita, Adolfo},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ACM DEV},
      keywords = {conference},
      pages = {17},
      title = {SAMo: Experimenting a Social Accountability Web Platform},
      year = {2013}
    }
    
  12. Ciaghi, A., Eshete, B., Molini, P., & Villafiorita, A. (2012). Social Accountability in Mozambique: an Experience Report from the Moamba District. In E-Infrastructures and E-Services on Developing Countries: Fourth International ICST and IEEE Conference, AFRICOMM 2012, Yaounde, Cameroon, November 12-14. Retrieved from http://www.ict4g.net/adolfo/downloads/papers/africomm12-samo.pdf [Abstract] [BibTeX] Download PDF...

    Abstract

    {Empowering citizens in making Governments more account- able and transparent in the services the provide has gained more atten- tion in the last few years both in the developing and in the developed world. At the basis of any such exercise, information and data collection activities play an important role. In this paper we report on a pilot we conducted in collaboration with the Ministry of Education, the World- Bank, the Maputo Living Lab, in the Moamba region of Mozambique to experiment with a platform we developed to collect data about various procurement indicators of primary schools in the region.}
    @inproceedings{CiaEshMol12,
      abstract = {Empowering citizens in making Governments more account- able and transparent in the services the provide has gained more atten- tion in the last few years both in the developing and in the developed world. At the basis of any such exercise, information and data collection activities play an important role. In this paper we report on a pilot we conducted in collaboration with the Ministry of Education, the World- Bank, the Maputo Living Lab, in the Moamba region of Mozambique to experiment with a platform we developed to collect data about various procurement indicators of primary schools in the region.},
      author = {Ciaghi, Aaron and Eshete, Birhanu and Molini, Pietro and Villafiorita, Adolfo},
      booktitle = {E-Infrastructures and E-Services on Developing Countries: Fourth International ICST and IEEE Conference, AFRICOMM 2012, Yaounde, Cameroon, November 12-14},
      keywords = {conference},
      title = {Social Accountability in Mozambique: an Experience Report from the Moamba District},
      topics = {social_accountability, ict4g, mozambique},
      url = {http://www.ict4g.net/adolfo/downloads/papers/africomm12-samo.pdf},
      year = {2012}
    }
    
  13. Sahilu, H., Villafiorita, A., Weldemariam, K., Belachew, M., & Zewge, A. (2012). Designing distributed agricultural information services for developing countries. In E. Cutrell, E. W. Zegura, G. Borriello, & B. Thies (Eds.), ACM DEV (p. 24). ACM. [Abstract] [BibTeX]

    Abstract

    {In developing countries, agriculture is the largest livelihood provider. Nevertheless, the vast majority of gains by farmers are unsatisfactory despite the efforts put into the agriculture cost inputs. At present smallholder farmers, farmers associations, consumers, intermediaries and supporting organizations (e.g., extension agencies) are often unable to engage effectively in agricultural markets since these markets are prone to inefficiencies. Small and subsistence farmers in particular tend to have unfavorable linkages to markets due to a lack of market orientation. They continue to rely on market information supplied and verified through traditional word-of-mouth approach. Many producers and smaller intermediaries also lack experience to effectively utilize such market information to improve their well-being.}
    @inproceedings{DBLP:conf/dev/SahiluVWBZ12,
      abstract = {In developing countries, agriculture is the largest livelihood provider. Nevertheless, the vast majority of gains by farmers are unsatisfactory despite the efforts put into the agriculture cost inputs. At present smallholder farmers, farmers associations, consumers, intermediaries and supporting organizations (e.g., extension agencies) are often unable to engage effectively in agricultural markets since these markets are prone to inefficiencies. Small and subsistence farmers in particular tend to have unfavorable linkages to markets due to a lack of market orientation. They continue to rely on market information supplied and verified through traditional word-of-mouth approach. Many producers and smaller intermediaries also lack experience to effectively utilize such market information to improve their well-being.},
      author = {Sahilu, Henok and Villafiorita, Adolfo and Weldemariam, Komminist and Belachew, Mesfin and Zewge, Amanuel},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ACM DEV},
      keywords = {conference},
      pages = {24},
      title = {Designing distributed agricultural information services for developing countries},
      topics = {ict4g, eagriculture},
      year = {2012}
    }
    
  14. Ciaghi, A., Valle, A. D., & Villafiorita, A. (2011). Adapting Software Metrics to Analyze the Evolution of Laws – An Italian Case Study. In K. M. Atkinson (Ed.), Frontiers in Artificial Intelligence and Applications (Vol. 235, pp. 53–62). IOS Press. Retrieved from http://www.ict4g.net/adolfo/downloads/papers/jurix-2011.pdf [Abstract] [BibTeX] Download PDF...

    Abstract

    {Law-makers, designers of legal information systems and citizens are often challenged by the complexity of bodies of law and the growing number of references needed to interpret a law. Quantifying this complexity is not an easy task. In this paper we present some analyses we conducted on the Italian body of laws, made available through the “Normattiva” website. Some of the metrics we applied are similar to those often used to measure the quality of software systems.}
    @inproceedings{Ciaghi:2011woa,
      abstract = {Law-makers, designers of legal information systems and citizens are often challenged by the complexity of bodies of law and the growing number of references needed to interpret a law. Quantifying this complexity is not an easy task. In this paper we present some analyses we conducted on the Italian body of laws, made available through the “Normattiva” website. Some of the metrics we applied are similar to those often used to measure the quality of software systems.},
      author = {Ciaghi, Aaron and Valle, Andrea Dalla and Villafiorita, Adolfo},
      booktitle = {Frontiers in Artificial Intelligence and Applications},
      editor = {Atkinson, Katie M.},
      keywords = {conference},
      month = dec,
      pages = {53-62},
      publisher = {IOS Press},
      title = {Adapting Software Metrics to Analyze the Evolution of Laws – An Italian Case Study},
      topics = {ict4laws, software_metrics},
      url = {http://www.ict4g.net/adolfo/downloads/papers/jurix-2011.pdf},
      volume = {235},
      year = {2011}
    }
    
  15. Asfaw, B., Bekele, D., Eshete, B., Villafiorita, A., & Weldemariam, K. (2010). Host-based anomaly detection for pervasive medical systems. In CRiSIS (pp. 1–8). IEEE. [Abstract] [BibTeX]

    Abstract

    {Intrusion detection systems are deployed on hosts in a computing infrastructure to tackle undesired events in the course of usage of the systems. One of the promising domains of applying intrusion detection is the healthcare domain. A typical healthcare scenario is characterized by high degree of mobility, frequent interruptions and above all demands access to sensitive medical records by concerned stakeholders. Migrating these set of concerns in pervasive healthcare environ- ment where the traditional characteristics are more intensified in terms of uncertainty, one ends up with more challenges on security due to nature of pervasive devices and wireless communication media along with classic security problems for desktop based systems. Despite evolution of automated healthcare services and sophistication of attacks against such services, there is a reasonable lack of techniques, tools and experimental setups for protecting hosts against intrusive actions. This paper presents a contribution to provide a host- based, anomaly modeling and detection approach based on data mining techniques for pervasive healthcare systems. The technique maintains normal usage profile of pervasive healthcare applications and inspects current workflow against normal usage profile so as to classify it as anomalous or normal. The technique is implemented as a prototype with sample data set and the results obtained revealed that the technique is able to perform classification of anomalous activities with acceptable accuracy.}
    @inproceedings{DBLP:conf/crisis/AsfawBEVW10,
      abstract = {Intrusion detection systems are deployed on hosts in a computing infrastructure to tackle undesired events in the course of usage of the systems. One of the promising domains of applying intrusion detection is the healthcare domain. A typical healthcare scenario is characterized by high degree of mobility, frequent interruptions and above all demands access to sensitive medical records by concerned stakeholders. Migrating these set of concerns in pervasive healthcare environ- ment where the traditional characteristics are more intensified in terms of uncertainty, one ends up with more challenges on security due to nature of pervasive devices and wireless communication media along with classic security problems for desktop based systems. Despite evolution of automated healthcare services and sophistication of attacks against such services, there is a reasonable lack of techniques, tools and experimental setups for protecting hosts against intrusive actions.  This paper presents a contribution to provide a host- based, anomaly modeling and detection approach based on data mining techniques for pervasive healthcare systems. The technique maintains normal usage profile of pervasive healthcare applications and inspects current workflow against normal usage profile so as to classify it as anomalous or normal. The technique is implemented as a prototype with sample data set and the results obtained revealed that the technique is able to perform classification of anomalous activities with acceptable accuracy.},
      author = {Asfaw, Biniyam and Bekele, Dawit and Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {CRiSIS},
      keywords = {conference},
      pages = {1-8},
      title = {Host-based anomaly detection for pervasive medical systems},
      topics = {security, ehealth},
      year = {2010}
    }
    
  16. Eshete, B., Villafiorita, A., & Weldemariam, K. (2011). Early Detection of Security Misconfiguration Vulnerabilities in Web Applications. In ARES (pp. 169–174). IEEE. [BibTeX]

    Abstract

    @inproceedings{DBLP:conf/aresec/EsheteVW11,
      author = {Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ARES},
      keywords = {conference},
      pages = {169-174},
      title = {Early Detection of Security Misconfiguration Vulnerabilities in Web Applications},
      topics = {security},
      year = {2011}
    }
    
  17. Ciaghi, A., & Villafiorita, A. (2012). Crowdsourcing ICTD Best Practices. In Springer (Ed.), E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24 (Vol. 92, pp. 167–176). Retrieved from http://ict4g.net/adolfo/downloads/papers/africomm11-crowdsourcing.pdf [Abstract] [BibTeX] Download PDF...

    Abstract

    {Most ICT for Development projects fail. We claim that most failures are due to an unstructured approach to software development. In this paper, we propose a crowdsourcing web portal to collect best practices from ICTD project managers and allow them to access a com- mon knowledge base. This will allow us to understand how to improve activities within the lifecycle of projects and design a software process for ICTD.}
    @inproceedings{Ciaghi:2012uq,
      abstract = {Most ICT for Development projects fail. We claim that most failures are due to an unstructured approach to software development. In this paper, we propose a crowdsourcing web portal to collect best practices from ICTD project managers and allow them to access a com- mon knowledge base. This will allow us to understand how to improve activities within the lifecycle of projects and design a software process for ICTD.},
      author = {Ciaghi, Aaron and Villafiorita, Adolfo},
      booktitle = {E-Infrastructures and E-Services on Developing Countries: Third International ICST Conference, AFRICOMM 2011, Zanzibar, Tanzania, November 23-24},
      editor = {Springer},
      keywords = {conference},
      month = mar,
      pages = {167-176},
      series = {LNICST},
      title = {Crowdsourcing ICTD Best Practices},
      topics = {ict4g, software_quality, software_engineering_process},
      url = {http://ict4g.net/adolfo/downloads/papers/africomm11-crowdsourcing.pdf},
      volume = {92},
      year = {2012}
    }
    
  18. Ciaghi, A., Villafiorita, A., Chemane, L., & Macueve, G. (2011). Stimulating Development through Transnational Living Labs: the Italo-Mozambican Vision. In Proceedings of the 6th Annual IST-Africa Conference Gabarone, Botswana. [Abstract] [BibTeX]

    Abstract

    {In this paper, we present the vision for Maputo Living Lab (MLL), which started in January 2011, as part of a network of Living Labs located in developed and in developing regions. The Maputo Living Lab has the purpose of activating a transfer of competences, innovation and education between Trentino (an Autonomous Province in Northern Italy), Mozambique and other developing countries. The tight connection between Mozambique and Trentino makes some characteristics of MLL unique in the Living Labs panorama and poses various challenges that we describe in this paper.}
    @inproceedings{Ciaghi:2011uq,
      abstract = {In this paper, we present the vision for Maputo Living Lab (MLL), which started in January 2011, as part of a network of Living Labs located in developed and in developing regions. The Maputo Living Lab has the purpose of activating a transfer of competences, innovation and education between Trentino (an Autonomous Province in Northern Italy), Mozambique and other developing countries. The tight connection between Mozambique and Trentino makes some characteristics of MLL unique in the Living Labs panorama and poses various challenges that we describe in this paper.},
      author = {Ciaghi, Aaron and Villafiorita, Adolfo and Chemane, Lourino and Macueve, Gertrudes},
      booktitle = {Proceedings of the 6th Annual IST-Africa Conference Gabarone, Botswana},
      keywords = {conference},
      month = may,
      title = {Stimulating Development through Transnational Living Labs: the Italo-Mozambican Vision},
      topics = {ict4g, living_labs, mozambique},
      year = {2011}
    }
    
  19. Ciaghi, A., & Villafiorita, A. (2011). Improving Public Administrations via Law Modeling and BPR. In Springer (Ed.), E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa. [Abstract] [BibTeX]

    Abstract

    {Semantic Web technologies can be used to produce concep- tual representations of legal documents and to perform reasoning on the information that they contain. At the same time, Business Process Re-engineering is being applied more frequently to optimize the procedures of Public Administrations. While the existing literature on tools and methodologies to analyze, model and manipulate legal documents is extensive, there is a lack of a comprehensive tool that allows for a complete analysis of laws in all their aspect. In this paper we propose the design of a modeling framework to support the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations.}
    @inproceedings{Ciaghi:2011fk,
      abstract = {Semantic Web technologies can be used to produce concep- tual representations of legal documents and to perform reasoning on the information that they contain. At the same time, Business Process Re-engineering is being applied more frequently to optimize the procedures of Public Administrations. While the existing literature on tools and methodologies to analyze, model and manipulate legal documents is extensive, there is a lack of a comprehensive tool that allows for a complete analysis of laws in all their aspect. In this paper we propose the design of a modeling framework to support the law-making process, facilitating the participation of people without a jurisprudence background to the editing of regulations.},
      author = {Ciaghi, Aaron and Villafiorita, Adolfo},
      booktitle = {E-Infrastructures and E-Services on Developing Countries: Second International ICST Conference, AFRICOMM 2010, Cape Town, South Africa},
      editor = {Springer},
      keywords = {conference},
      month = oct,
      title = {Improving Public Administrations via Law Modeling and BPR},
      topics = {business_process_reengineering, ict4laws},
      year = {2011}
    }
    
  20. Weldemariam, K., Villafiorita, A., & Mattioli, A. (2009). Experiments and data analysis of electronic voting system. In A. A. E. Kalam, Y. Deswarte, & M. Mostafa (Eds.), CRiSIS (pp. 105–112). IEEE. [Abstract] [BibTeX]

    Abstract

    {During the last four years we have been involved in the development, experimentation, and evaluation of an electronic voting (e-voting) system. The system tried out in several regular elections, and also used in two small elections with legal value. Each experiment provided various sociological (e.g. citizens’ opinions on the system) and technical data that are related to system’s performance and behavior. This paper presents various technical insights and the lesson learned during the e-voting experiment. This helps to confirm existing data on the subject (e.g., data related to security, procedures and logistics) and, in some cases, provide novel information or, at least, shed a new perspective on some security-critical factors concerning e-voting systems.}
    @inproceedings{DBLP:conf/crisis/WeldemariamVM09,
      abstract = {During the last four years we have been involved in the development, experimentation, and evaluation of an electronic voting (e-voting) system. The system tried out in several regular elections, and also used in two small elections with legal value. Each experiment provided various sociological (e.g. citizens’ opinions on the system) and technical data that are related to system’s performance and behavior. This paper presents various technical insights and the lesson learned during the e-voting experiment. This helps to confirm existing data on the subject (e.g., data related to security, procedures and logistics) and, in some cases, provide novel information or, at least, shed a new perspective on some security-critical factors concerning e-voting systems.},
      author = {Weldemariam, Komminist and Villafiorita, Adolfo and Mattioli, Andrea},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {CRiSIS},
      keywords = {conference},
      pages = {105-112},
      title = {Experiments and data analysis of electronic voting system},
      topics = {evoting},
      year = {2009}
    }
    
  21. Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2009). Formal analysis of attacks for e-voting system. In A. A. E. Kalam, Y. Deswarte, & M. Mostafa (Eds.), CRiSIS (pp. 26–34). IEEE. [Abstract] [BibTeX]

    Abstract

    {Recently, the use of formal methods to specify and verify properties of electronic voting (e-voting) systems, with particular interest in security, verifiability, and anonymity, is getting much attention. Formal specification and verification of such systems can greatly help to better understand the system requirements by thoroughly specifying and analyzing the underlying assumptions and security specific properties. Unfortunately, even though these systems have been formally verified to satisfy the desired system security requirements, they are still vulnerable to attack. In this paper we extend a formal specification of the ES&S voting system by specifying attacks that have been shown to successfully compromise the system. We believe that performing such analysis is important for two reasons: first, it allows us to discover some missing critical requirements for the specification and/or assumptions that were not met. Second, it allows us to derive mitigation or counter-measure strategies when the system behaves differently than it should. We used the ASTRAL language for the specification, and the verification is performed using the PVS tool.}
    @inproceedings{DBLP:conf/crisis/WeldemariamKV09,
      abstract = {Recently, the use of formal methods to specify and verify properties of electronic voting (e-voting) systems, with particular interest in security, verifiability, and anonymity, is getting much attention. Formal specification and verification of such systems can greatly help to better understand the system requirements by thoroughly specifying and analyzing the underlying assumptions and security specific properties. Unfortunately, even though these systems have been formally verified to satisfy the desired system security requirements, they are still vulnerable to attack.  In this paper we extend a formal specification of the ES&S voting system by specifying attacks that have been shown to successfully compromise the system. We believe that performing such analysis is important for two reasons: first, it allows us to discover some missing critical requirements for the specification and/or assumptions that were not met. Second, it allows us to derive mitigation or counter-measure strategies when the system behaves differently than it should. We used the ASTRAL language for the specification, and the verification is performed using the PVS tool.},
      author = {Weldemariam, Komminist and Kemmerer, Richard A. and Villafiorita, Adolfo},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {CRiSIS},
      keywords = {conference},
      pages = {26-34},
      title = {Formal analysis of attacks for e-voting system},
      topics = {evoting, formal_methods, security},
      year = {2009}
    }
    
  22. Weldemariam, K., & Villafiorita, A. (2010). A Survey: Electronic Voting Development and Trends. In R. Krimmer & R. Grimm (Eds.), Electronic Voting (Vol. 167, pp. 119–131). GI. [Abstract] [BibTeX]

    Abstract

    {Any practitioner working on electronic voting (e-voting) seem to have stumbled upon the main issues that seem to affect the area. On the one hand —given the criticality and the risk e-voting systems potentially pose to the democratic process— e-voting systems are permanently under a magnifying glass that amplifies any glitch, be it significant or not. On the other hand, given the interest e-voting raises with the general public, there seems to be a tendency to generalize and oversimplify. This tendency leads to attribute specific problems to all systems, regardless of context, situation, and actual systems used. Additionally, scarce know-how about the electoral context often contributes to make matters even more confused. This is not to say all e-voting systems show the security and reliability characteristics that are necessary for system of such a criticality. On the contrary, a lot of work still has to be done. Starting from previous experiences and from a large-scale experimentation we conducted in Italy, this paper provides some directions, issues, and trends in e-voting. Getting a clearer view of the research activities in the area, highlighting both positive and negative results, and emphasizing some trends, could help, in our opinion, drawing a neater line between opinion from facts and contribute to the construction of a next generation of e-voting machines to be safely and more confidently employed for elections. }
    @inproceedings{DBLP:conf/ev/WeldemariamV10,
      abstract = {Any practitioner working on electronic voting (e-voting) seem to have stumbled upon the main issues that seem to affect the area. On the one hand —given the criticality and the risk e-voting systems potentially pose to the democratic process— e-voting systems are permanently under a magnifying glass that amplifies any glitch, be it significant or not. On the other hand, given the interest e-voting raises with the general public, there seems to be a tendency to generalize and oversimplify. This tendency leads to attribute specific problems to all systems, regardless of context, situation, and actual systems used. Additionally, scarce know-how about the electoral context often contributes to make matters even more confused.  This is not to say all e-voting systems show the security and reliability characteristics that are necessary for system of such a criticality. On the contrary, a lot of work still has to be done.  Starting from previous experiences and from a large-scale experimentation we conducted in Italy, this paper provides some directions, issues, and trends in e-voting. Getting a clearer view of the research activities in the area, highlighting both positive and negative results, and emphasizing some trends, could help, in our opinion, drawing a neater line between opinion from facts and contribute to the construction of a next generation of e-voting machines to be safely and more confidently employed for elections.  },
      author = {Weldemariam, Komminist and Villafiorita, Adolfo},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {Electronic Voting},
      keywords = {conference},
      pages = {119-131},
      title = {A Survey: Electronic Voting Development and Trends},
      topics = {evoting},
      year = {2010}
    }
    
  23. Villafiorita, A., Weldemariam, K., Susi, A., & Siena, A. (2010). Modeling and Analysis of Laws Using BPR and Goal-Oriented Framework. In L. Berntzen, F. Bodendorf, E. Lawrence, M. Perry, & Åsa Smedberg (Eds.), ICDS (pp. 353–358). IEEE Computer Society. [Abstract] [BibTeX]

    Abstract

    {Recently, two complementary approaches are proposed to represent, model, and analyze laws: the Nomos and VLPM approaches. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal re- alization for requirements guided by satisfiability of normative propositions obtained from rules embedded in a law. The latter offers a tool supported (re-)engineering methodology to extract laws represented in XML and build models using a subset of UML diagrams. Both allow traceability between laws and their respective models. This paper proposes an integration of these two approaches. We believe that this provides a framework that allows to trace and reason either top-down, from principles to their implementation or, viceversa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than a simple juxtaposition of the two techniques.}
    @inproceedings{DBLP:conf/icds/VillafioritaWSS10,
      abstract = {Recently, two complementary approaches are proposed to represent, model, and analyze laws: the Nomos and VLPM approaches. Nomos is a goal-oriented approach to effectively capture high-level principles in terms of goal re- alization for requirements guided by satisfiability of normative propositions obtained from rules embedded in a law. The latter offers a tool supported (re-)engineering methodology to extract laws represented in XML and build models using a subset of UML diagrams. Both allow traceability between laws and their respective models.  This paper proposes an integration of these two approaches. We believe that this provides a framework that allows to trace and reason either top-down, from principles to their implementation or, viceversa, bottom-up, from a change in the procedure to the principles. It is exactly this connection that adds value to the solution we propose and makes our approach more significant than a simple juxtaposition of the two techniques.},
      author = {Villafiorita, Adolfo and Weldemariam, Komminist and Susi, Angelo and Siena, Alberto},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ICDS},
      keywords = {conference},
      note = {Best paper award},
      pages = {353-358},
      title = {Modeling and Analysis of Laws Using BPR and Goal-Oriented Framework},
      topics = {ict4laws, business_process_reengineering},
      year = {2010}
    }
    
  24. Bekele, D., Eshete, B., Villafiorita, A., & Weldemariam, K. (2010). Context Information Refinement for Pervasive Medical Systems. In L. Berntzen, F. Bodendorf, E. Lawrence, M. Perry, & Åsa Smedberg (Eds.), ICDS (pp. 210–215). IEEE Computer Society. [Abstract] [BibTeX]

    Abstract

    {Emerging technologies like mobile and wireless communication are offering promising opportunities to enable mobile healthcare delivery to citizens. But, enhancing the qual- ity of service of such systems demands systematic improvement of existing service infrastructure. In this paper, we describe a context information refinement architecture proposed to address the shortcomings of existing works in relation to context information refinement in pervasive medical systems. The shortcomings are lack of adequate consideration for: quality parameters of context information, relevance of context information and particular requirements of the pervasive healthcare domain. The proposed architecture facilitates and coordinates the refinement of context infor- mation starting from acquisition of context information up until the refined context information is delivered to the target application in a pervasive medical system. We developed a prototype that implements the core components of the proposed architecture and evaluated it with real-life pervasive healthcare scenario and proved the validity of the architecture using a real-life scenario.}
    @inproceedings{DBLP:conf/icds/BekeleEVW10,
      abstract = {Emerging technologies like mobile and wireless communication are offering promising opportunities to enable mobile healthcare delivery to citizens. But, enhancing the qual- ity of service of such systems demands systematic improvement of existing service infrastructure.  In this paper, we describe a context information refinement architecture proposed to address the shortcomings of existing works in relation to context information refinement in pervasive medical systems. The shortcomings are lack of adequate consideration for: quality parameters of context information, relevance of context information and particular requirements of the pervasive healthcare domain. The proposed architecture facilitates and coordinates the refinement of context infor- mation starting from acquisition of context information up until the refined context information is delivered to the target application in a pervasive medical system. We developed a prototype that implements the core components of the proposed architecture and evaluated it with real-life pervasive healthcare scenario and proved the validity of the architecture using a real-life scenario.},
      author = {Bekele, Dawit and Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ICDS},
      keywords = {conference},
      note = {Best paper award},
      pages = {210-215},
      title = {Context Information Refinement for Pervasive Medical Systems},
      topics = {ehealth},
      year = {2010}
    }
    
  25. Eshete, B., Mattioli, A., Villafiorita, A., & Weldemariam, K. (2010). ICT for Good: Opportunities, Challenges and the Way Forward. In L. Berntzen, F. Bodendorf, E. Lawrence, M. Perry, & Åsa Smedberg (Eds.), ICDS (pp. 14–19). IEEE Computer Society. [Abstract] [BibTeX]

    Abstract

    {ICT seems well understood as a tool and an infrastructure for delivering information and services for the society and for allowing communications through interactions among the service users —mostly, the digital society. Using ICT for ensuring better life requires far more than good infrastructure, ICT know-how and the various techniques and tools in place. If ICT has to address the real problems of the society, it should be at a rescue being environment-friendly, with real and tangible impact, sustainable, seamless, down to the grass-roots and above all with reproducible experiences. In this paper, we introduce a different perspective of looking into and using ICT, which we call ICT for Good (ICT4G). It is about using ICT for addressing problems of societies with low ICT penetration and changing a society’s life for the better. More specifically, based on our observation of current promises ICT gives to society, we discuss ICT4G’s distinguishing aspects, opportunities it offers, challenges it imposes along with preliminary roadmap for its realization. A high-level correlation of what we pointed out with a relevant case study (i.e., the eGIF4M1) is presented.}
    @inproceedings{DBLP:conf/icds/EsheteMVW10,
      abstract = {ICT seems well understood as a tool and an infrastructure for delivering information and services for the society and for allowing communications through interactions among the service users —mostly, the digital society. Using ICT for ensuring better life requires far more than good infrastructure, ICT know-how and the various techniques and tools in place. If ICT has to address the real problems of the society, it should be at a rescue being environment-friendly, with real and tangible impact, sustainable, seamless, down to the grass-roots and above all with reproducible experiences.  In this paper, we introduce a different perspective of looking into and using ICT, which we call ICT for Good (ICT4G). It is about using ICT for addressing problems of societies with low ICT penetration and changing a society’s life for the better. More specifically, based on our observation of current promises ICT gives to society, we discuss ICT4G’s distinguishing aspects, opportunities it offers, challenges it imposes along with preliminary roadmap for its realization. A high-level correlation of what we pointed out with a relevant case study (i.e., the eGIF4M1) is presented.},
      author = {Eshete, Birhanu and Mattioli, Andrea and Villafiorita, Adolfo and Weldemariam, Komminist},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ICDS},
      keywords = {conference},
      pages = {14-19},
      title = {ICT for Good: Opportunities, Challenges and the Way Forward},
      topics = {ict4g},
      year = {2010}
    }
    
  26. Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2010). Formal Specification and Analysis of an E-voting System. In ARES (pp. 164–171). IEEE Computer Society. [Abstract] [BibTeX]

    Abstract

    {Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.}
    @inproceedings{DBLP:conf/IEEEares/WeldemariamKV10,
      abstract = {Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws.  The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties.  This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.},
      author = {Weldemariam, Komminist and Kemmerer, Richard A. and Villafiorita, Adolfo},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {ARES},
      keywords = {conference},
      pages = {164-171},
      title = {Formal Specification and Analysis of an E-voting System},
      topics = {evoting, security, formal_methods},
      year = {2010}
    }
    
  27. Ciaghi, A., Weldemariam, K., Villafiorita, A., Mattioli, A., & Quoc-Phan, S. (2010). Supporting Public Administration with an Integrated BPR Environment. In A. Villafiorita, S.-P. Regis, & A. Zorer (Eds.), E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM 2009, Maputo, Mozambique. Springer. [Abstract] [BibTeX]

    Abstract

    {The definition or redesign of Public Administration (PA) procedures is particularly challenging. This is, for example, due to the requirement of cooperation of different organizational units and actors, different laws and procedures for the production of several artifacts, and maintaining traceability while integrating processes with new laws. We are interested in business process modeling and re-engineering (BPR) for PA, where ICT can play a pivotal role by, e.g., improving communication among law-makers and process analysts. With regard to this previously we developed a tool called VLPM1. The tool is designed to provide assistance in BPR for PA, which allows traceability between laws and processes. In this paper, we discuss the extension of the tool and of its methodology to support an integrated environment that can be used for better law and process redesign by performing formal analysis on the processes. We discuss its system components and provide a working example taken from the Italian Immigration law, as a proof of concept.}
    @inproceedings{Ciaghi:2009xb,
      abstract = {The definition or redesign of Public Administration (PA) procedures is particularly challenging. This is, for example, due to the requirement of cooperation of different organizational units and actors, different laws and procedures for the production of several artifacts, and maintaining traceability while integrating processes with new laws.  We are interested in business process modeling and re-engineering (BPR) for PA, where ICT can play a pivotal role by, e.g., improving communication among law-makers and process analysts. With regard to this previously we developed a tool called VLPM1. The tool is designed to provide assistance in BPR for PA, which allows traceability between laws and processes. In this paper, we discuss the extension of the tool and of its methodology to support an integrated environment that can be used for better law and process redesign by performing formal analysis on the processes. We discuss its system components and provide a working example taken from the Italian Immigration law, as a proof of concept.},
      author = {Ciaghi, Aaron and Weldemariam, Komminist and Villafiorita, Adolfo and Mattioli, Andrea and Quoc-Phan, Sang},
      booktitle = {E-Infrastructures and E-Services on Developing Countries: First International ICST Conference, AFRICOMM 2009, Maputo, Mozambique},
      editor = {Villafiorita, Adolfo and Regis, Saint-Paul and Zorer, Alessandro},
      keywords = {conference},
      month = jun,
      publisher = {Springer},
      title = {Supporting Public Administration with an Integrated BPR Environment},
      topics = {business_process_reengineering, ict4laws},
      year = {2010}
    }
    
  28. Shvaiko, P., Villafiorita, A., Zorer, A., Chemane, L., Fumo, T., & Hinkkanen, J. (2009). eGIF4M: eGovernment Interoperability Framework for Mozambique. In M. Wimmer, H. J. Scholl, M. Janssen, & R. Traunmüller (Eds.), EGOV (Vol. 5693, pp. 328–340). Springer. Retrieved from http://ict4g.net/adolfo/downloads/papers/egif4m-2009.pdf [Abstract] [BibTeX] Download PDF...

    Abstract

    {Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of re- sources, is a complex technical and organizational challenge. The prob- lem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. This paper presents eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term.}
    @inproceedings{DBLP:conf/egov/ShvaikoVZCFH09,
      abstract = {Harmonizing decentralized development of ICT solutions with centralized strategies, e.g., meant to favor reuse and optimization of re- sources, is a complex technical and organizational challenge. The prob- lem, shared by virtually all the governments, is becoming a priority also for countries, such as Mozambique, that have started their ICT policy relatively recently and for which it is now evident that — if no particular attention is devoted to the interoperability of the solutions being developed — the result will rapidly become a patchwork of solutions incompatible with each other. This paper presents eGIF4M: eGovernment Interoperability Framework for Mozambique. The framework is based on a holistic approach. It builds on top of the existing experiences in eGIFs all over the world and it addresses some specific needs and peculiarities of developing countries, like Mozambique. The result is a comprehensive framework based on: (i) a reference architecture along with technical standards, (ii) a standardization life cycle, (iii) a maturity model, and (iv) some key actions meant to make the initiative sustainable in the longer term.},
      author = {Shvaiko, Pavel and Villafiorita, Adolfo and Zorer, Alessandro and Chemane, Lourino and Fumo, Teotónio and Hinkkanen, Jussi},
      bibsource = {DBLP, http://dblp.uni-trier.de},
      booktitle = {EGOV},
      keywords = {conference},
      pages = {328-340},
      title = {eGIF4M: eGovernment Interoperability Framework for Mozambique},
      topics = {egovernment, interoperability, ict4g},
      url = {http://ict4g.net/adolfo/downloads/papers/egif4m-2009.pdf},
      year = {2009}
    }
    
  29. Weldemariam, K. S., & Villafiorita, A. (2008). A Methodology for Assessing Procedural Security: A Case Study in E-Voting. In Electronic Voting (pp. 83–94). GI. [Abstract] [BibTeX]

    Abstract

    {The organization of elections in Italy involves various offices of the Public Administration and private contractors, has a time-span of months, and has strict security and traceability requirements. Sensibility by citizens and politicians is very high, and litigation over, e.g., implementation of procedures and validity of results are not uncommon. In this paper we present a methodology for procedural security assessment in order to analyze and eventually make election secure. Our approach is based on modeling the nominal procedures implementation in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable specification and perform the analysis. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. undetected attacks) and to identify more precisely under what hypotheses we can guaran- tee secure elections. We demonstrate our approach with the help of an excerpt of e-Voting system scenario that it is derived from the current experimentation of the Italian legislation.}
    @inproceedings{Weldemariam:2008ee,
      abstract = {The organization of elections in Italy involves various offices of the Public Administration and private contractors, has a time-span of months, and has strict security and traceability requirements. Sensibility by citizens and politicians is very high, and litigation over, e.g., implementation of procedures and validity of results are not uncommon. In this paper we present a methodology for procedural security assessment in order to analyze and eventually make election secure. Our approach is based on modeling the nominal procedures implementation in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable specification and perform the analysis. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. undetected attacks) and to identify more precisely under what hypotheses we can guaran- tee secure elections. We demonstrate our approach with the help of an excerpt of e-Voting system scenario that it is derived from the current experimentation of the Italian legislation.},
      author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo},
      booktitle = {Electronic Voting},
      keywords = {conference},
      location = {Bregenz, Austria},
      pages = {83–94},
      publisher = {GI},
      series = {Lecture Notes in Informatics (LNI)},
      title = {A Methodology for Assessing Procedural Security: A Case Study in E-Voting},
      topics = {procedural_security_analysis, evoting},
      year = {2008}
    }
    
  30. Weldemariam, K. S., & Villafiorita, A. (2008). Formal Procedural Security Modeling and Analysis. In Proceedings of 3rd International Conference on Risks and Security of Internet and Systems (CriSiS’08) (pp. 249–254). IEEE. [Abstract] [BibTeX]

    Abstract

    {We are involved in a project related to the evaluation and possible introduction of e-voting for elections held in the Autonomous Province of Trento. One of the goals of the project is defining the laws and the procedures that will regulate e-voting and guarantee the same or an higher level of security than the traditional, paper-based, elections. To do so, we are tackling the problem (also) at the procedural level, namely, we are trying to understand weaknesses and strengths of the procedures regulating elections in Italy, in order to analyze possible attacks and their effects. The analyses are based on formal specifications of the procedures and on model checkers to help us derive possible attacks. We believe the approach to be useful to help us systematically identifying the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and, con- sequently, to state more precisely under what hypotheses and conditions we can guarantee reasonably secure elections.}
    @inproceedings{Weldemariam:2008qf,
      abstract = {We are involved in a project related to the evaluation and possible introduction of e-voting for elections held in the Autonomous Province of Trento. One of the goals of the project is defining the laws and the procedures that will regulate e-voting and guarantee the same or an higher level of security than the traditional, paper-based, elections. To do so, we are tackling the problem (also) at the procedural level, namely, we are trying to understand weaknesses and strengths of the procedures regulating elections in Italy, in order to analyze possible attacks and their effects. The analyses are based on formal specifications of the procedures and on model checkers to help us derive possible attacks. We believe the approach to be useful to help us systematically identifying the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and, con- sequently, to state more precisely under what hypotheses and conditions we can guarantee reasonably secure elections.},
      annote = {Publik Printout available},
      author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo},
      booktitle = {Proceedings of 3rd International Conference on Risks and Security of Internet and Systems (CriSiS’08)},
      keywords = {conference},
      location = {Tozeur, Tunisia},
      pages = {249–254},
      publisher = {IEEE},
      title = {Formal Procedural Security Modeling and Analysis},
      topics = {procedural_security_analysis, evoting},
      year = {2008}
    }
    
  31. Weldemariam, K. S., Villafiorita, A., & Mattioli, A. (2007). Assessing Procedural Risks and Threats in e-Voting: Challenges and an Approach. In E-Voting and Identity, First International Conference, VOTE-ID 2007 (Vol. 4896, pp. 38–49). Springer Berlin / Heidelberg: Springer. [Abstract] [BibTeX]

    Abstract

    {Performing a good security analysis on the design of a system is an essential step in order to guarantee a reasonable level of protection. However, different attacks and threats may be carried out depending on the operational environment in which the system is used, i.e. the pro- cedures that define how to operate the systems. Using strong-passwords to limit access to a system is useless — to make a simple example — if users are allowed to write the passwords on paper and leave them near the computers they operate. We are interested in reasoning about the security of e-Voting procedures, namely on the risks and attacks that can be carried out during an elec- tion. Our focus is more on people and organizations than on systems and technologies. In this paper we describe some ongoing work that we are carrying out within the ProVotE project (a project sponsored by the Autonomous Province of Trento to switch to e-Voting for local elections) to analyze and (possibly) improve procedural security of electronic elections. To do so, we are we are providing models of the Italian electoral laws using the UML and we are developing a custom methodology for analyzing threats from the models. Our reasoning approach is based on asset mobility, asset values and existence of multiple instances.}
    @inproceedings{Weldemariam:2007hq,
      abstract = {Performing a good security analysis on the design of a system is an essential step in order to guarantee a reasonable level of protection. However, different attacks and threats may be carried out depending on the operational environment in which the system is used, i.e. the pro- cedures that define how to operate the systems. Using strong-passwords to limit access to a system is useless — to make a simple example — if users are allowed to write the passwords on paper and leave them near the computers they operate.  We are interested in reasoning about the security of e-Voting procedures, namely on the risks and attacks that can be carried out during an elec- tion. Our focus is more on people and organizations than on systems and technologies.  In this paper we describe some ongoing work that we are carrying out within the ProVotE project (a project sponsored by the Autonomous Province of Trento to switch to e-Voting for local elections) to analyze and (possibly) improve procedural security of electronic elections. To do so, we are we are providing models of the Italian electoral laws using the UML and we are developing a custom methodology for analyzing threats from the models. Our reasoning approach is based on asset mobility, asset values and existence of multiple instances.},
      address = {Springer Berlin / Heidelberg},
      annote = {Publik Printout NOT available},
      author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo and Mattioli, Andrea},
      booktitle = {E-Voting and Identity, First International Conference, VOTE-ID 2007},
      isbn = {978-3-540-77492-1},
      keywords = {conference},
      pages = {38–49},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Assessing Procedural Risks and Threats in e-Voting: Challenges and an Approach},
      topics = {procedural_security_analysis, evoting},
      volume = {4896},
      year = {2007}
    }
    
  32. Weldemariam, K. S., & Villafiorita, A. (2008). Modeling and Analysis of Procedural Security in (e)Voting: the Trentino’s Approach and Experiences. In Proceedings of the conference on Electronic voting technology (pp. 1–10). Berkeley, CA, USA: USENIX Association. Retrieved from https://www.usenix.org/legacy/event/evt08/tech/full_papers/weldemariam/weldemariam.pdf [Abstract] [BibTeX] Download PDF...

    Abstract

    {This paper describes the experiences and the challenges we are facing within the ProVotE project, a four years project sponsored by the Autonomous Province of Trento that has the goal of switching to e-voting for local elections. One of the activities we are carrying out within ProVotE is the systematic analysis of the weaknesses and strengths of the procedures regulating local elections in Italy, in order to derive possible attacks and their effects. The approach we take is based on providing formal specifications of the procedures and using model checkers to help us analyze the effects of attacks. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and to identify more precisely under what hypotheses and conditions we can guarantee reasonably secure electronic elections. This paper presents the methodology and the techniques we are devising and experimenting with to tackle problem highlighted above.}
    @inproceedings{Weldemariam:2008ay,
      abstract = {This paper describes the experiences and the challenges we are facing within the ProVotE project, a four years project sponsored by the Autonomous Province of Trento that has the goal of switching to e-voting for local elections. One of the activities we are carrying out within ProVotE is the systematic analysis of the weaknesses and strengths of the procedures regulating local elections in Italy, in order to derive possible attacks and their effects. The approach we take is based on providing formal specifications of the procedures and using model checkers to help us analyze the effects of attacks. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. under what hypotheses attacks are undetectable) and to identify more precisely under what hypotheses and conditions we can guarantee reasonably secure electronic elections. This paper presents the methodology and the techniques we are devising and experimenting with to tackle problem highlighted above.},
      address = {Berkeley, CA, USA},
      annote = {Publik Printout available on the internet},
      author = {Weldemariam, Komminist Sisai and Villafiorita, Adolfo},
      booktitle = {Proceedings of the conference on Electronic voting technology},
      keywords = {conference},
      location = {San Jose, USA},
      pages = {1–10},
      publisher = {USENIX Association},
      title = {Modeling and Analysis of Procedural Security in (e)Voting: the Trentino’s Approach and Experiences},
      topics = {procedural_security_analysis, evoting},
      url = {https://www.usenix.org/legacy/event/evt08/tech/full_papers/weldemariam/weldemariam.pdf},
      year = {2008}
    }
    
  33. Sebastiani, R., & Villafiorita, A. (1998). SAT-based decision procedures for normal modal logics: a theoretical framework. In Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98). Springer. [BibTeX]

    Abstract

    @inproceedings{Sebastiani:1998dw,
      annote = {Publik Printout available},
      author = {Sebastiani, Roberto and Villafiorita, Adolfo},
      booktitle = {Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98)},
      keywords = {conference},
      location = {Sozopol, Bulgaria},
      publisher = {Springer},
      title = {SAT-based decision procedures for normal modal logics: a theoretical framework},
      topics = {theorem_proving},
      year = {1998}
    }
    
  34. Bozzano, M., & Villafiorita, A. (2003). Improving System Reliability via Model Checking: the FSAP/NuSMV-SA Safety Analysis Platform. In Proceedings of the 22nd International Confecence SAFECOMP 2003 (Vol. 2788, pp. 49–62). Springer. [Abstract] [BibTeX]

    Abstract

    {Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMV- SA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionality of FSAP/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analy- sis for Complex Systems), an European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development.}
    @inproceedings{Bozzano:2003bl,
      abstract = {Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMV- SA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionality of FSAP/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analy- sis for Complex Systems), an European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development.},
      annote = {Publik Printout available},
      author = {Bozzano, Marco and Villafiorita, Adolfo},
      booktitle = {Proceedings of the 22nd International Confecence SAFECOMP 2003},
      keywords = {conference},
      location = {Edinburgh, Scotland},
      pages = {49–62},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Improving System Reliability via Model Checking: the FSAP/NuSMV-SA Safety Analysis Platform},
      topics = {avionics, safety_analysis, formal_methods, safety_critical_systems},
      volume = {2788},
      year = {2003}
    }
    
  35. Volha, B., Dalpiaz, F., Ferrario, R., Mattioli, A., & Villafiorita, A. (2007). Evaluating Procedural Alternatives: a case study in e-voting. In Proceedings of 1st International Conference on Methodologies, Technologies and Tools Enabling e-Government (MeTTeG07) (pp. 125–138). Halley. [Abstract] [BibTeX]

    Abstract

    {This paper describes part of the work carried out within the ProVotE project. It presents the approach we are taking in order to provide both precise models of the electoral processes of an electronic voting, and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures to support the provincial elections of 2008. In particular, the approach is based on defining an alternating sequence of models, written using UML and Tropos. The former is used to represent the electoral processes (both existing and future), while the latter is meant to provide design rationale for the taken decisions about the future procedures. The choice is made after having evaluated the available alternatives against non-functional requirements with the help of Tropos goal analysis techniques.}
    @inproceedings{Volha:2007bv,
      abstract = {This paper describes part of the work carried out within the ProVotE project. It presents the approach we are taking in order to provide both precise models of the electoral processes of an electronic voting, and mechanisms for documenting and reasoning on the possible alternative implementations of the procedures to support the provincial elections of 2008. In particular, the approach is based on defining an alternating sequence of models, written using UML and Tropos. The former is used to represent the electoral processes (both existing and future), while the latter is meant to provide design rationale for the taken decisions about the future procedures. The choice is made after having evaluated the available alternatives against non-functional requirements with the help of Tropos goal analysis techniques.},
      annote = {Publik Printout available},
      author = {Volha, Bryl and Dalpiaz, Fabiano and Ferrario, Roberta and Mattioli, Andrea and Villafiorita, Adolfo},
      booktitle = {Proceedings of 1st International Conference on Methodologies, Technologies and Tools Enabling e-Government (MeTTeG07)},
      keywords = {conference},
      month = sep,
      pages = {125–138},
      publisher = {Halley},
      title = {Evaluating Procedural Alternatives: a case study in e-voting},
      topics = {procedural_security_analysis, evoting},
      year = {2007}
    }
    
  36. Ciaghi, A., Mattioli, A., & Villafiorita, A. (2009). VLPM: a Tool to support BPR in Public Administration. In Proceedings of the Third International Conference on Digital Society (ICDS2009) (pp. 289–293). IEEE Computer Society. [Abstract] [BibTeX]

    Abstract

    {Representing a law defining some procedures by means of workflow diagrams has various advantages: it facilitates the understanding of the actual meaning of its text, it helps to build a shared vision between law-makers and officers of the Public Administration, and it provides an easier way to analyze and make Public Administration procedures more efficient. To keep the model understandable and maintainable, however, the need soon arises to keep traceability between the workflow diagrams and the laws from which the workflows are derived. Moreover – since the public administration processes are defined and regulated by laws – when the workflows are the target of a re-engineering activity, such traceability information becomes essential to identify what laws need to be changed to implement the new procedures. This paper presents VLPM (Visual Law Process Modeler). It is a tool that addresses some of the issues mentioned above and that we have used to model the laws regulating the introduction of an electronic election in Friuli Venezia Giulia, one of the Autonomous Regions of Italy. VLPM is built on top of the UML Visual Paradigm tool and it is freely available}
    @inproceedings{Ciaghi:2009os,
      abstract = {Representing a law defining some procedures by means of workflow diagrams has various advantages: it facilitates the understanding of the actual meaning of its text, it helps to build a shared vision between law-makers and officers of the Public Administration, and it provides an easier way to analyze and make Public Administration procedures more efficient.  To keep the model understandable and maintainable, however, the need soon arises to keep traceability between the workflow diagrams and the laws from which the workflows are derived. Moreover – since the public administration processes are defined and regulated by laws – when the workflows are the target of a re-engineering activity, such traceability information becomes essential to identify what laws need to be changed to implement the new procedures.  This paper presents VLPM (Visual Law Process Modeler). It is a tool that addresses some of the issues mentioned above and that we have used to model the laws regulating the introduction of an electronic election in Friuli Venezia Giulia, one of the Autonomous Regions of Italy. VLPM is built on top of the UML Visual Paradigm tool and it is freely available},
      annote = {Publik Printout NOT available},
      author = {Ciaghi, Aaron and Mattioli, Andrea and Villafiorita, Adolfo},
      booktitle = {Proceedings of the Third International Conference on Digital Society (ICDS2009)},
      keywords = {conference},
      location = {Cancun, Mexico},
      note = {Best paper award},
      pages = {289–293},
      publisher = {IEEE Computer Society},
      title = {VLPM: a Tool to support BPR in Public Administration},
      topics = {business_process_reengineering, egovernment},
      year = {2009}
    }
    
  37. Giunchiglia, F., & Villafiorita, A. (1996). ABSFOL: A Proof Checker with Abstraction. In Proceedings of the 13th International Conference on Automated Deduction (CADE13) (Vol. 1104, pp. 136–140). Springer. [Abstract] [BibTeX]

    Abstract

    {Intuitively, an abstraction is a mapping from a representation of a problem onto a new representation. ABSFOL is an interactive theorem built on top of GETFOL that supports abstraction. In this paper we demonstrate the use of the tool through an example taken from Boolean Algebra.}
    @inproceedings{Giunchiglia:1996jo,
      abstract = {Intuitively, an abstraction is a mapping from a representation of a problem onto a new representation.  ABSFOL is an interactive theorem built on top of GETFOL that supports abstraction. In this paper we demonstrate the use of the tool through an example taken from Boolean Algebra.},
      annote = {Publik Printout available},
      author = {Giunchiglia, Fausto and Villafiorita, Adolfo},
      booktitle = {Proceedings of the 13th International Conference on Automated Deduction (CADE13)},
      keywords = {conference},
      location = {New Brunswick, NJ, USA},
      month = jul,
      pages = {136–140},
      publisher = {Springer},
      series = {Lecture Notes in Artificial Intelligence},
      title = {ABSFOL: A Proof Checker with Abstraction},
      topics = {abstraction, theorem_proving, ABSFOL},
      volume = {1104},
      year = {1996}
    }
    
  38. Chiappini, A., Cimatti, A., Porzia, C., Rotondo, G., Sebastiani, R., Traverso, P., & Villafiorita, A. (1999). Formal Specification and Development of a Safety-Critical Train Management. In Proceedings of 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999) (pp. 410–419). Springer. [Abstract] [BibTeX]

    Abstract

    {In this paper we describe the on-going specification and development of Ansaldo’s Radio Block Center (RBC), a component of the next-generation European Rail Traffic Management System (ERTMS). The RBC will be responsible of managing the movement of trains equipped with radio communication. Its development process is critical: the RBC is a large-scale and complex system, it must provide several novel services at different levels of functionality, it must guarantee interoperability according to European standards, and, last but not least, a high level of safety. We have addressed these issues by devising a development based on formal specifications. ERTMS scenarios have been formalized in order to provide a better understanding of the interoperability requirements. The architecture of the RBC has been formally specified such that the system can be incrementally built as an overlay system (compatible with the existing train detection and interlocking systems) and modularly expanded to control different kinds of trains. The formal specifications of the behaviour of each RBC module have been structured hierarchically: they provide an easy-to-understand documentation for customers and developers; moreover, they can be simulated and validated automatically at the early stage of the development process, thus providing a high level of confidence in their safety in a cost-effective way. }
    @inproceedings{Chiappini:1999dk,
      abstract = {In this paper we describe the on-going specification and development of Ansaldo’s Radio Block Center (RBC), a component of the next-generation European Rail Traffic Management System (ERTMS).  The RBC will be responsible of managing the movement of trains equipped with radio communication.  Its development process is critical: the RBC is a large-scale and complex system, it must provide several novel services at different levels of functionality, it must guarantee interoperability according to European standards, and, last but not least, a high level of safety. We have addressed these issues by devising a development based on formal specifications.  ERTMS scenarios have been formalized in order to provide a better understanding of the interoperability requirements. The architecture of the RBC has been formally specified such that the system can be incrementally built as an overlay system (compatible with the existing train detection and interlocking systems) and modularly expanded to control different kinds of trains.  The formal specifications of the behaviour of each RBC module have been structured hierarchically: they provide an easy-to-understand documentation for customers and developers; moreover, they can be simulated and validated automatically at the early stage of the development process, thus providing a high level of confidence in their safety in a cost-effective way.  },
      annote = {Publik Printout available},
      author = {Chiappini, Angelo and Cimatti, Alessandro and Porzia, Carmen and Rotondo, Gianni and Sebastiani, Roberto and Traverso, Paolo and Villafiorita, Adolfo},
      booktitle = {Proceedings of 18th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1999)},
      keywords = {conference},
      location = {Toulouse, France},
      month = sep,
      pages = {410–419},
      publisher = {Springer},
      title = {Formal Specification and Development of a Safety-Critical Train Management},
      topics = {railways, formal_methods, safety_critical_systems},
      year = {1999}
    }
    
  39. Longo, F., Tiella, R., Tonella, P., & Villafiorita, A. (2008). Measuring the Impact of Different Categories of Software Evolution. In IWSM/Metrikon/Mensura (Vol. 5338, pp. 344–351). Springer. [Abstract] [BibTeX]

    Abstract

    {Software evolution involves different categories of interventions, having variable impact on the code. Knowledge about the expected impact of an intervention is fundamental for project planning and resource allocation. Moreover, deviations from the expected impact may hint for areas of the system having a poor design. In this paper, we investigate the relationship between evolution categories and impacted code by means of a set of metrics computed over time for a subject system }
    @inproceedings{Longo:2008jw,
      abstract = {Software evolution involves different categories of interventions, having variable impact on the code. Knowledge about the expected impact of an intervention is fundamental for project planning and resource allocation. Moreover, deviations from the expected impact may hint for areas of the system having a poor design. In this paper, we investigate the relationship between evolution categories and impacted code by means of a set of metrics computed over time for a subject system },
      annote = {Publik Printout NOT available},
      author = {Longo, Francesca and Tiella, Roberto and Tonella, Paolo and Villafiorita, Adolfo},
      booktitle = {IWSM/Metrikon/Mensura},
      keywords = {conference},
      location = {Munich, Germany},
      pages = {344–351},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      title = {Measuring the Impact of Different Categories of Software Evolution},
      topics = {software_quality, software_metrics},
      volume = {5338},
      year = {2008}
    }
    
  40. Giunchiglia, F., Sebastiani, R., Villafiorita, A., & Walsh, T. (1996). A General Purpose Reasoner for Abstraction. In Proceedings of Advances in Artificial Intelligence, 11th Biennal Conference of the Canadian Society for Computational Studies of Intelligence (AI96) (Vol. 1081, pp. 323–335). Springer. [Abstract] [BibTeX]

    Abstract

    {The goal of the work described in this paper is the development of a system, called ABSFOL, which allows the user to state declaratively abstractions and to use them according to the desired control strategy. ABSFOL has been successfully tested on many examples. So far we have failed to find an interesting abstraction whose implementation requires a major programming effort.}
    @inproceedings{Giunchiglia:1996yo,
      abstract = {The goal of the work described in this paper is the development of a system, called ABSFOL, which allows the user to state declaratively abstractions and to use them according to the desired control strategy. ABSFOL has been successfully tested on many examples. So far we have failed to find an interesting abstraction whose implementation requires a major programming effort.},
      annote = {Publik Printout available},
      author = {Giunchiglia, Fausto and Sebastiani, Roberto and Villafiorita, Adolfo and Walsh, Toby},
      booktitle = {Proceedings of Advances in Artificial Intelligence, 11th Biennal Conference of the Canadian Society for Computational Studies of Intelligence (AI96)},
      keywords = {conference},
      location = {Toronto, Ontario, Canada},
      month = may,
      pages = {323–335},
      publisher = {Springer},
      series = {Lecture Notes in Artificial Intelligence},
      title = {A General Purpose Reasoner for Abstraction},
      topics = {abstraction, theorem_proving},
      volume = {1081},
      year = {1996}
    }
    
  41. Bozzano, M., Cavallo, A., Cifaldi, M., Valacca, L., & Villafiorita, A. (2003). Improving Safety Assessment of Complex Systems: An Industrial case study. In Proceedings of the International Symposium of Formal Methods Europe (FME 2003) (Vol. 2805, pp. 208–222). Springer-Verlag. [Abstract] [BibTeX]

    Abstract

    {The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a corresponding increase in the capability of design and safety engineers to maintain adequate safety levels. The use of formal methods during system design has proved to be effective in several practical applications. The development of certain classes of applications, like, for instance, avionic system, however, also requires to analyse the behaviour of a system under certain degraded situations (e.g. when some components are not working as expected). This step, usually performed by safety engineers in a set of dedicated activities, has the goal of pointing out what are all the possible causes of a system malfunction or, more properly, a hazard of the system. It is an essential step to obtain the high safety levels required to keep public confidence in system behaviour, according to the current procedures for system certification (e.g., ARP4754). The integration of system design activities with safety assessment and the use of formal notations for the safety assessment of a system, although not new, are still at an early stage. These goals are addressed by the ESACS project, a European-Union-sponsored project grouping several industrial companies from the aeronautic field. The ESACS project is developing a methodology and a platform the ESACS platform that helps safety engineers automating certain phases of their work. An integral part of the project is the evaluation of the methodology and of the platform on a set of industrial case studies. This paper reports on the application of the ESACS methodology and on the use of the ESACS platform to one of such case studies, namely, the Secondary Power System of the Eurofighter Typhoon aircraft.}
    @inproceedings{Bozzano:2003vh,
      abstract = {The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a corresponding increase in the capability of design and safety engineers to maintain adequate safety levels. The use of formal methods during system design has proved to be effective in several practical applications. The development of certain classes of applications, like, for instance, avionic system, however, also requires to analyse the behaviour of a system under certain degraded situations (e.g. when some components are not working as expected). This step, usually performed by safety engineers in a set of dedicated activities, has the goal of pointing out what are all the possible causes of a system malfunction or, more properly, a hazard of the system. It is an essential step to obtain the high safety levels required to keep public confidence in system behaviour, according to the current procedures for system certification (e.g., ARP4754). The integration of system design activities with safety assessment and the use of formal notations for the safety assessment of a system, although not new, are still at an early stage. These goals are addressed by the ESACS project, a European-Union-sponsored project grouping several industrial companies from the aeronautic field. The ESACS project is developing a methodology and a platform the ESACS platform that helps safety engineers automating certain phases of their work. An integral part of the project is the evaluation of the methodology and of the platform on a set of industrial case studies. This paper reports on the application of the ESACS methodology and on the use of the ESACS platform to one of such case studies, namely, the Secondary Power System of the Eurofighter Typhoon aircraft.},
      annote = {Publik Printout available},
      author = {Bozzano, Marco and Cavallo, Antonella and Cifaldi, Massimo and Valacca, Laura and Villafiorita, Adolfo},
      booktitle = {Proceedings of the International Symposium of Formal Methods Europe (FME 2003)},
      keywords = {conference},
      location = {Pisa, Italy},
      pages = {208–222},
      publisher = {Springer-Verlag},
      series = {Lecture Notes in Computer Science},
      title = {Improving Safety Assessment of Complex Systems: An Industrial case study},
      topics = {avionics, safety_analysis, formal_methods, safety_critical_systems},
      volume = {2805},
      year = {2003}
    }
    
  42. Bozzano, M., Villafiorita, A., Akerlund, O., Bieber, P., Bougnol, C., Boede, E., … Cifaldi, M. (2003). ESACS: an integrated methodology for design and safety analysis of complex systems. In Proceedings of the European Safety and Reliability Conference 2003, ESREL2003. Balkema. [Abstract] [BibTeX]

    Abstract

    {The continuous increase of system complexity — stimulated by the higher complexity of the functionality provided by software-based embedded controllers and by the huge improvement in the computational power of hardware — requires a corresponding increase in the capability of design and safety engineers to maintain adequate safety and reliability levels. Emerging techniques, like formal methods, have the potential of dealing with the growing complexity of such systems and are increasingly being used for the development of critical systems (e.g. aircraft systems, nuclear plants, railways systems), where at stake are not only delays in delivering products and economical losses, but also environmental hazards and public confidence. However, the use of formal meth- ods during certain critical system development phases, e.g. safety analysis, is still at an early stage. In this paper we propose a new methodology, based on these novel techniques and supported by commercial and state-of-the-art tools, whose goal is to improve the safety analysis practices carried out during the development and certification of complex systems. The key ingredient of our methodology is the use of formal methods during both system development and safety analysis. This allows for a tighter integration of safety assessment and system development activities, fast system prototyping, automated safety assessment since the early stages of development, and tool- supported verification and validation.}
    @inproceedings{Bozzano:2003fe,
      abstract = {The continuous increase of system complexity — stimulated by the higher complexity of the functionality provided by software-based embedded controllers and by the huge improvement in the computational power of hardware — requires a corresponding increase in the capability of design and safety engineers to maintain adequate safety and reliability levels. Emerging techniques, like formal methods, have the potential of dealing with the growing complexity of such systems and are increasingly being used for the development of critical systems (e.g. aircraft systems, nuclear plants, railways systems), where at stake are not only delays in delivering products and economical losses, but also environmental hazards and public confidence. However, the use of formal meth- ods during certain critical system development phases, e.g. safety analysis, is still at an early stage. In this paper we propose a new methodology, based on these novel techniques and supported by commercial and state-of-the-art tools, whose goal is to improve the safety analysis practices carried out during the development and certification of complex systems. The key ingredient of our methodology is the use of formal methods during both system development and safety analysis. This allows for a tighter integration of safety assessment and system development activities, fast system prototyping, automated safety assessment since the early stages of development, and tool- supported verification and validation.},
      annote = {Publik Printout available},
      author = {Bozzano, Marco and Villafiorita, Adolfo and Akerlund, Ove and Bieber, Pierre and Bougnol, C. and Boede, Eckard and Bretschneider, Matthias and Cavallo, Antonella and Castel, C. and Cifaldi, Massimo},
      booktitle = {Proceedings of the European Safety and Reliability Conference 2003, ESREL2003},
      keywords = {conference},
      location = {Maastricht, The Netherlands},
      publisher = {Balkema},
      title = {ESACS: an integrated methodology for design and safety analysis of complex systems},
      topics = {avionics, safety_analysis, safety_critical_systems},
      year = {2003}
    }
    
  43. Bozzano, M., & Villafiorita, A. (2003). Integrating Fault Tree Analysis with Event Ordering Information. In Proceedings of the European Safety and Reliability Conference 2003 (ESREL 2003). Balkema. [Abstract] [BibTeX]

    Abstract

    {Fault tree analysis is a traditional and well-established technique for analyzing system design and robustness. Its purpose is to identify sets of basic events, called cut sets, which can cause a given top level event, e.g., a system malfunction, to occur. In this paper we present an algorithm that extracts ordering infor- mation, i.e., finds out possible ordering constraints which are required to hold between basic events in a cut set. The algorithm is completely automatic, and has been incorporated into a more general framework, based on model checking techniques, for automatic fault tree generation and analysis.}
    @inproceedings{Bozzano:2003ts,
      abstract = {Fault tree analysis is a traditional and well-established technique for analyzing system design and robustness. Its purpose is to identify sets of basic events, called cut sets, which can cause a given top level event, e.g., a system malfunction, to occur. In this paper we present an algorithm that extracts ordering infor- mation, i.e., finds out possible ordering constraints which are required to hold between basic events in a cut set. The algorithm is completely automatic, and has been incorporated into a more general framework, based on model checking techniques, for automatic fault tree generation and analysis.},
      annote = {Publik Printout available},
      author = {Bozzano, Marco and Villafiorita, Adolfo},
      booktitle = {Proceedings of the European Safety and Reliability Conference 2003 (ESREL 2003)},
      keywords = {conference},
      location = {Maastricht, The Netherlands},
      publisher = {Balkema},
      title = {Integrating Fault Tree Analysis with Event Ordering Information},
      topics = {avionics, safety_analysis, formal_methods, safety_critical_systems},
      year = {2003}
    }
    
  44. Villafiorita, A. (1998). Abstraction as a Form of Elaboration Tolerance. In Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98) (pp. 427–437). Springer. [Abstract] [BibTeX]

    Abstract

    {Elaboration tolerance is "the ability of accepting changes to a person’s or a computer program’s representation of facts without starting all over" [8]. In this paper we investigate how abstraction (in the sense of [5]) helps in achieving a certain degree of elaboration tolerance. We do so by mechanizing in absfol (an interactive theorem prover with abstraction) two famous representations of the missionaries and canni- bals problem and by showing how abstraction helps in finding solutions in such representations ". . . without starting all over."}
    @inproceedings{Villafiorita:1998pb,
      abstract = {Elaboration tolerance is "the ability of accepting changes to a person’s or a computer program’s representation of facts without starting all over" [8]. In this paper we investigate how abstraction (in the sense of [5]) helps in achieving a certain degree of elaboration tolerance. We do so by mechanizing in absfol (an interactive theorem prover with abstraction) two famous representations of the missionaries and canni- bals problem and by showing how abstraction helps in finding solutions in such representations ". . . without starting all over."},
      annote = {Publik Printout available},
      author = {Villafiorita, Adolfo},
      booktitle = {Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA98)},
      keywords = {conference},
      location = {Sozopol, Bulgaria},
      pages = {427–437},
      publisher = {Springer},
      title = {Abstraction as a Form of Elaboration Tolerance},
      topics = {abstraction, theorem_proving},
      year = {1998}
    }
    
  45. Cimatti, A., Pieraccini, P. L., Sebastiani, R., Traverso, P., & Villafiorita, A. (1999). Formal Specification and validation of a Vital Communication Protocol. In Proceedings of FM99, World Congress on Formal methods in the Development of Computing Systems (pp. 1584–1604). Springer. [BibTeX]

    Abstract

    @inproceedings{Cimatti:1999xr,
      annote = {Publik Printout available},
      author = {Cimatti, Alessandro and Pieraccini, Pier Luigi and Sebastiani, Roberto and Traverso, Paolo and Villafiorita, Adolfo},
      booktitle = {Proceedings of FM99, World Congress on Formal methods in the Development of Computing Systems},
      keywords = {conference},
      location = {Toulouse, France},
      month = sep,
      pages = {1584–1604},
      publisher = {Springer},
      title = {Formal Specification and validation of a Vital Communication Protocol},
      topics = {railways, formal_methods, safety_critical_systems},
      year = {1999}
    }
    
  46. Tiella, R., Villafiorita, A., & Tomasi, S. (2007). FSMC+, a tool for the generation of Java code from statecharts. In Proceedings of the 5th international symposium on Principles and practice of programming in Java (PPPJ-07) (pp. 93–102). ACM. [Abstract] [BibTeX]

    Abstract

    {ProVotE is a two-phase project aiming at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections in Trentino (Nov. 2008). During the first phase of the ProVotE project we built jprovote, a Java/Linux e-voting system. The jprovote system has been used with experimental value by more than 11000 voters during local elections held in various municipalities of Trentino (Italy). A critical component of jprovote is its core logic, that is responsible of controlling the overall behavior of the e-voting machine during an election. In order to simplify its development and to allow for formal verification of this critical component we developed FSMC+. FSMC+ is a compiler that takes as input a subset of UML Statecharts and produces the corresponding Java and NuSMV code (NuSMV is a model checker developed at ITC-irst). Support for parameters in events, complex expressions in guards, and support to nested states are some of the distinguishing features of FSMC+. In this paper we present FSMC+ and we show how we used it for the development and the verification of the ProVotE e-voting machine. Even though FSMC+ has been specifically created to ease the development of jProvote, we believe the approach and the tool we developed to be general enough to be used in other applications.}
    @inproceedings{Tiella:2007kb,
      abstract = {ProVotE is a two-phase project aiming at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections in Trentino (Nov. 2008). During the first phase of the ProVotE project we built jprovote, a Java/Linux e-voting system. The jprovote system has been used with experimental value by more than 11000 voters during local elections held in various municipalities of Trentino (Italy).  A critical component of jprovote is its core logic, that is responsible of controlling the overall behavior of the e-voting machine during an election. In order to simplify its development and to allow for formal verification of this critical component we developed FSMC+.  FSMC+ is a compiler that takes as input a subset of UML Statecharts and produces the corresponding Java and NuSMV code (NuSMV is a model checker developed at ITC-irst). Support for parameters in events, complex expressions in guards, and support to nested states are some of the distinguishing features of FSMC+. In this paper we present FSMC+ and we show how we used it for the development and the verification of the ProVotE e-voting machine. Even though FSMC+ has been specifically created to ease the development of jProvote, we believe the approach and the tool we developed to be general enough to be used in other applications.},
      annote = {Publik Printout available},
      author = {Tiella, Roberto and Villafiorita, Adolfo and Tomasi, Silvia},
      booktitle = {Proceedings of the 5th international symposium on Principles and practice of programming in Java (PPPJ-07)},
      keywords = {conference},
      location = {Lisboa, Portugal},
      month = sep,
      pages = {93–102},
      publisher = {ACM},
      title = {FSMC+, a tool for the generation of Java code from statecharts},
      topics = {formal_methods, evoting},
      year = {2007}
    }
    

workshop

  1. Grau, I., Travassos, G., Cernuzzi, L., & Villafiorita, A. (2014). Tape Mbo’e: A First Experimental Assessment. In 11th Experimental Software Engineering Track Workshop (ESELAW), XVII Ibero-American Conference on Software Engineering (CIbSE). [Abstract] [BibTeX]

    Abstract

    {The development of software needs not only to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions such as service oriented must be considered as the basic architecture style to build sustainable applications into environments were practitioners are not aware of this software technology. Besides this, most of the available software processes are not direct applicable neither reusable making the learning time risky to the development of the project. Therefore, Tape Mbo’e (TME) had been proposed to strive the building of such applications, into development environments like developing country where we can have economic constraints and scarcity of proficient practitioners. TME is being used to develop a software application whose goal is to provide the interoperability among legacy systems of distinct public agencies in Paraguay. To observe TME’s use, observational studies have been executed to reveal TME’s feasibility and applicability in supporting public agencies to organize their software projects. Initial results indicated the feasibility and simplicity of TME when applied in the field. Therefore, an experience accomplished into a Paraguayan public agency is presented in this paper.}
    @inproceedings{GR-14,
      abstract = {The development of software needs not only to consider the construction process, but also other aspects such as cost, human resources and communication among stakeholders. The lack of simplicity into this context becomes explicit when some restrictions such as service oriented must be considered as the basic architecture style to build sustainable applications into environments were practitioners are not aware of this software technology. Besides this, most of the available software processes are not direct applicable neither reusable making the learning time risky to the development of the project. Therefore, Tape Mbo’e (TME) had been proposed to strive the building of such applications, into development environments like developing country where we can have economic constraints and scarcity of proficient practitioners.  TME is being used to develop a software application whose goal is to provide the interoperability among legacy systems of distinct public agencies in Paraguay. To observe TME’s use, observational studies have been executed to reveal TME’s feasibility and applicability in supporting public agencies to organize their software projects. Initial results indicated the feasibility and simplicity of TME when applied in the field. Therefore, an experience accomplished into a Paraguayan public agency is presented in this paper.},
      author = {Grau, I. and Travassos, G. and Cernuzzi, L. and Villafiorita, A.},
      booktitle = {11th Experimental Software Engineering Track Workshop (ESELAW), XVII Ibero-American Conference on Software Engineering (CIbSE)},
      keywords = {workshop},
      month = apr,
      owner = {Ilse},
      timestamp = {2014.10.21},
      title = {Tape Mbo’e: A First Experimental Assessment},
      year = {2014}
    }
    
  2. Weldemariam, K., Mattioli, A., & Villafiorita, A. (2009). Managing Requirements for E-Voting Systems: Issues and Approaches Motivated by a Case Study. In Requirements Engineering for e-Voting Systems (RE-VOTE), 2009 First International Workshop on (pp. 29–37). http://doi.org/10.1109/RE-VOTE.2009.7 [Abstract] [BibTeX]

    Abstract

    {This paper discusses our approach and experiences on structuring and maintaining requirements for an e- voting system we have built and deployed for elections. Issues related to integrating laws and recommendation for e-voting systems, managing different elections and configurations, supporting a spiral development, yielded problems and approaches to help maintain integrity of requirements and a coherent view of the system. Moreover, the relationship between requirements and system architecture is based on finite state machines, that bridge the gap between the laws and the actual behavior of the machine.}
    @inproceedings{5460389,
      abstract = {This paper discusses our approach and experiences on structuring and maintaining requirements for an e- voting system we have built and deployed for elections. Issues related to integrating laws and recommendation for e-voting systems, managing different elections and configurations, supporting a spiral development, yielded problems and approaches to help maintain integrity of requirements and a coherent view of the system. Moreover, the relationship between requirements and system architecture is based on finite state machines, that bridge the gap between the laws and the actual behavior of the machine.},
      author = {Weldemariam, Komminist and Mattioli, Andrea and Villafiorita, Adolfo},
      booktitle = {Requirements Engineering for e-Voting Systems (RE-VOTE), 2009 First International Workshop on},
      doi = {10.1109/RE-VOTE.2009.7},
      keywords = {workshop},
      month = aug,
      pages = {29 -37},
      title = {Managing Requirements for E-Voting Systems: Issues and Approaches Motivated by a Case Study},
      topics = {evoting},
      year = {2009}
    }
    
  3. Al-Shammari, A. F. N., Weldemariam, K., Villafiorita, A., & Tessaris, S. (2011). Vote verification through open standard: A roadmap. In Requirements Engineering for Electronic Voting Systems (REVOTE), 2011 International Workshop on (pp. 22–26). http://doi.org/10.1109/REVOTE.2011.6045912 [Abstract] [BibTeX]

    Abstract

    {As the technology for e-voting changes day by day along with an evolution of the regulatory environment, many questions emerge. One of these questions is how to allow voters or any third party to verify votes are correctly captured, stored and counted. This underlines the fact that an e-voting system is not only responsible for ensuring its technical and procedural security, but also must provide a mechanism by which voters can verify their votes during and after casting, and third party be able to verify the correctness and integrity of election results. The purpose of this paper is to review currently deployed vote verification methods, by discuss their weaknesses with the aim of proposing a more reliable and robust vote verification method.}
    @inproceedings{6045912,
      abstract = {As the technology for e-voting changes day by day along with an evolution of the regulatory environment, many questions emerge. One of these questions is how to allow voters or any third party to verify votes are correctly captured, stored and counted. This underlines the fact that an e-voting system is not only responsible for ensuring its technical and procedural security, but also must provide a mechanism by which voters can verify their votes during and after casting, and third party be able to verify the correctness and integrity of election results. The purpose of this paper is to review currently deployed vote verification methods, by discuss their weaknesses with the aim of proposing a more reliable and robust vote verification method.},
      author = {Al-Shammari, Ali Fawzi Najm and Weldemariam, Komminist and Villafiorita, Adolfo and Tessaris, Sergio},
      booktitle = {Requirements Engineering for Electronic Voting Systems (REVOTE), 2011 International Workshop on},
      doi = {10.1109/REVOTE.2011.6045912},
      keywords = {workshop},
      month = aug,
      pages = {22 -26},
      title = {Vote verification through open standard: A roadmap},
      topics = {evoting},
      year = {2011}
    }
    
  4. Eshete, B., Villafiorita, A., & Weldemariam, K. (2011). Malicious Website Detection: Effectiveness and Efficiency Issues. In Proceedings of SysSec 2011. Amsterdam. [Abstract] [BibTeX]

    Abstract

    {Malicious websites, when visited by an unsuspecting victim infect her machine to steal invaluable information, redirect her to malicious targets or compromise her system to mount future attacks. While the existing approaches have promising prospects in detecting malicious websites, there are still open issues in effectively and efficiently addressing: filtering of web pages from the wild, coverage of wide range of malicious characteristics to capture the big picture, continuous evolution of web page features, systematic combination of fea- tures, semantic implications of feature values on characterizing web pages, ease and cost of flexibility and scalability of analysis and detection techniques with respect to inevitable changes to the threat landscape. In this position paper, we highlight our ongoing efforts towards effective and efficient analysis and detection of malicious websites with a particular emphasis on broader feature space and attack-payloads, flexibility of techniques with changes in malicious characteristics and web pages and above all real-life usability of techniques in defending users against malicious websites.}
    @inproceedings{Eshete:2011fk,
      abstract = {Malicious websites, when visited by an unsuspecting victim infect her machine to steal invaluable information, redirect her to malicious targets or compromise her system to mount future attacks. While the existing approaches have promising prospects in detecting malicious websites, there are still open issues in effectively and efficiently addressing: filtering of web pages from the wild, coverage of wide range of malicious characteristics to capture the big picture, continuous evolution of web page features, systematic combination of fea- tures, semantic implications of feature values on characterizing web pages, ease and cost of flexibility and scalability of analysis and detection techniques with respect to inevitable changes to the threat landscape. In this position paper, we highlight our ongoing efforts towards effective and efficient analysis and detection of malicious websites with a particular emphasis on broader feature space and attack-payloads, flexibility of techniques with changes in malicious characteristics and web pages and above all real-life usability of techniques in defending users against malicious websites.},
      address = {Amsterdam},
      author = {Eshete, Birhanu and Villafiorita, Adolfo and Weldemariam, Komminist},
      booktitle = {Proceedings of SysSec 2011},
      keywords = {workshop},
      month = jul,
      title = {Malicious Website Detection: Effectiveness and Efficiency Issues},
      topics = {security},
      year = {2011}
    }
    
  5. Ciaghi, A., & Villafiorita, A. (2010). Towards a Law Modeling Framework to Support Law-Making via BPR. In Proceedings of the First Workshop on Law Compliancy Issues in Organisational Systems and Strategies. [Abstract] [BibTeX]

    Abstract

    {This paper presents a law modeling framework called VLPM 2.0 that aims at providing support to the application of BPR on Public Administration procedures. The tool leverages the existing technologies for legal documents markup and for process modeling and relies on semantic technologies to bind process model elements to elements in the texts. In this paper we discuss the motivations and the possible roles of such framework in the lifecycle of laws.}
    @inproceedings{Ciaghi:2010fk,
      abstract = {This paper presents a law modeling framework called VLPM 2.0 that aims at providing support to the application of BPR on Public Administration procedures. The tool leverages the existing technologies for legal documents markup and for process modeling and relies on semantic technologies to bind process model elements to elements in the texts. In this paper we discuss the motivations and the possible roles of such framework in the lifecycle of laws.},
      author = {Ciaghi, Aaron and Villafiorita, Adolfo},
      booktitle = {Proceedings of the First Workshop on Law Compliancy Issues in Organisational Systems and Strategies},
      keywords = {workshop},
      title = {Towards a Law Modeling Framework to Support Law-Making via BPR},
      topics = {ict4laws, business_process_reengineering},
      year = {2010}
    }
    
  6. Cimatti, A., Pieraccini, P. L., Sebastiani, R., Traverso, P., & Villafiorita, A. (1999). Formal Specification and validation of a Vital Communication Protocol. In Proceedings of 4th International ERCIM Workshop on Formal Methods for Industrial Critical Systems. [BibTeX]

    Abstract

    @inproceedings{Cimatti:1999xz,
      annote = { Printout available},
      author = {Cimatti, Alessandro and Pieraccini, Pier Luigi and Sebastiani, Roberto and Traverso, Paolo and Villafiorita, Adolfo},
      booktitle = {Proceedings of 4th International ERCIM Workshop on Formal Methods for Industrial Critical Systems},
      keywords = {workshop},
      title = {Formal Specification and validation of a Vital Communication Protocol},
      topics = {safety_critical_systems, railways, formal_methods},
      year = {1999}
    }
    
  7. Roveri, M., & Villafiorita, A. (1996). Using Abstraction to Prove Theorems in Boolean Algebra. In Proceedings of AISB96 Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice (pp. 40–41). [Abstract] [BibTeX]

    Abstract

    {We use abstraction as a tool to simplify proofs in Boolean Algebra (BA). We mechanize proofs by abstraction in- side ABSFOL. We use OTTER to assess the effectiveness of our approach.}
    @inproceedings{Roveri:1996fi,
      abstract = {We use abstraction as a tool to simplify proofs in Boolean Algebra (BA). We mechanize proofs by abstraction in- side ABSFOL. We use OTTER to assess the effectiveness of our approach.},
      annote = {Printout available},
      author = {Roveri, Marco and Villafiorita, Adolfo},
      booktitle = {Proceedings of AISB96 Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice},
      keywords = {workshop},
      location = {Brighton, UK},
      month = apr,
      pages = {40-41},
      title = {Using Abstraction to Prove Theorems in Boolean Algebra},
      topics = {abstraction, theorem_proving, boolean_algebra, ABSFOL},
      year = {1996}
    }
    
  8. Villafiorita, A., & Giunchiglia, F. (1996). Inductive Theorem Proving via Abstraction. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH96). [Abstract] [BibTeX]

    Abstract

    {We use abstraction as a tool to plan proofs by induction inside ABSFOL, an interactive theorem prover with abstraction}
    @inproceedings{Villafiorita:1996xw,
      abstract = {We use abstraction as a tool to plan proofs by induction inside ABSFOL, an interactive theorem prover with abstraction},
      annote = {Publik Printout available},
      author = {Villafiorita, Adolfo and Giunchiglia, Fausto},
      booktitle = {Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH96)},
      keywords = {workshop},
      location = {Fort Lauderdale, Florida},
      month = jan,
      title = {Inductive Theorem Proving via Abstraction},
      topics = {abstraction, theorem_proving, induction, ABSFOL},
      year = {1996}
    }
    
  9. Tiella, R., Villafiorita, A., & Tomasi, S. (2006). Specification of the Control Logic of an eVoting System in UML: the ProVotE experience. In Proceedings of 5th International Workshop on Critical Systems Development Using Modeling Languages (CSDUML06). [Abstract] [BibTeX]

    Abstract

    {The ProVotE project aims at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections. The goals of the project are building an e-voting system and defining the related process and certification issues in order to deliver a solution which is compliant with the italian electoral law, that is trusted and usable by the voters, and that implements the security and dependability requirements of the best international practices and experiences. This paper presents some of the issues and challenges we faced during the development of the e-voting prototype which was tested by about 8500 voters in three different trials held during the elections for the local representatives. In particular we show how we integrated UML in the development process of the e-voting machine. We also highlight how we extended existing tools to support the formal verification of the UML specifications and how we automated the generation of a critical component of the e-voting machine using UML statecharts.}
    @inproceedings{Tiella:2006ec,
      abstract = {The ProVotE project aims at actuating art. 84 of law 2 - 5/3/2003 of the Autonomous Province of Trento (Italy), which promotes the introduction of e-voting systems for the next provincial elections. The goals of the project are building an e-voting system and defining the related process and certification issues in order to deliver a solution which is compliant with the italian electoral law, that is trusted and usable by the voters, and that implements the security and dependability requirements of the best international practices and experiences.  This paper presents some of the issues and challenges we faced during the development of the e-voting prototype which was tested by about 8500 voters in three different trials held during the elections for the local representatives. In particular we show how we integrated UML in the development process of the e-voting machine. We also highlight how we extended existing tools to support the formal verification of the UML specifications and how we automated the generation of a critical component of the e-voting machine using UML statecharts.},
      annote = {Publik Printout available},
      author = {Tiella, Roberto and Villafiorita, Adolfo and Tomasi, Silvia},
      booktitle = {Proceedings of 5th International Workshop on Critical Systems Development Using Modeling Languages (CSDUML06)},
      keywords = {workshop},
      location = {Genova, Italy},
      month = oct,
      title = {Specification of the Control Logic of an eVoting System in UML: the ProVotE experience},
      topics = {software_quality, software_engineering_process, evoting, formal_methods},
      year = {2006}
    }
    
  10. Sebastiani, R., Villafiorita, A., & Giunchiglia, F. (1994). Proving Theorems by Using Abstraction Interactively. In Proceedings of the Second International Round-Table on Abstract Intelligent Agent: Situation Assessment (AIA 94). [Abstract] [BibTeX]

    Abstract

    {In this paper we show how an interactive use of abstraction in theorem proving can improve the comprehension and reduce the complexity of many significant problems. For such a task we present a fully mechanized example of the very well-know map colouring problem.}
    @inproceedings{Sebastiani:1994xd,
      abstract = {In this paper we show how an interactive use of abstraction in theorem proving can improve the comprehension and reduce the complexity of many significant problems. For such a task we present a fully mechanized example of the very well-know map colouring problem.},
      annote = {Publik Two printouts available (AIA + Scriftenreihe)},
      author = {Sebastiani, Roberto and Villafiorita, Adolfo and Giunchiglia, Fausto},
      booktitle = {Proceedings of the Second International Round-Table on Abstract Intelligent Agent: Situation Assessment (AIA 94)},
      keywords = {workshop},
      title = {Proving Theorems by Using Abstraction Interactively},
      topics = {abstraction, theorem_proving, ABSFOL},
      year = {1994}
    }
    
  11. Villafiorita, A., & Sebastiani, R. (1994). Proof planning by abstraction. In Proceedings of ECAI94 Workshop "From Theorem Provers to Mathematical Assistants" (pp. 15–24). [Abstract] [BibTeX]

    Abstract

    {Devising powerful heuristics or shifting the control to humans have probably been the two most common solutions to keep the search space in theorem proving manage- able. In this paper we take advantage of both, by using abstraction as a tool to plan proofs by induction and by proving its effectiveness in ABSFOL (an interactive theorem prover built on top of GETFOL}
    @inproceedings{Villafiorita:1994fy,
      abstract = {Devising powerful heuristics or shifting the control to humans have probably been the two most common solutions to keep the search space in theorem proving manage- able. In this paper we take advantage of both, by using abstraction as a tool to plan proofs by induction and by proving its effectiveness in ABSFOL (an interactive theorem prover built on top of GETFOL},
      annote = {Publik Printout available},
      author = {Villafiorita, Adolfo and Sebastiani, Roberto},
      booktitle = {Proceedings of ECAI94 Workshop "From Theorem Provers to Mathematical Assistants"},
      keywords = {workshop},
      location = {Amsterdam, The Netherlands},
      month = aug,
      pages = {15–24},
      title = {Proof planning by abstraction},
      topics = {abstraction, theorem_proving, ABSFOL},
      year = {1994}
    }
    
  12. Cimatti, A., Giunchiglia, F., Traverso, P., & Villafiorita, A. (1999). Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study. In Proceedings of FLoC99 Workshop on Run-Time Result Verification. [Abstract] [BibTeX]

    Abstract

    {In this paper we describe an industrial project whose goal was the certification of the translator part of a tool used to develop safety critical applications. We have successfully applied a novel formal verification technique. We have constructed an Embedded Verifier which, for each run of the translator, verifies formally the correctness of the result of each translation, rather than the correctness of the translation algorithm or code. We call this approach Run-time Result Formal Verification. In order to satisfy efficiency requirements on the Embedded Verifier, we have decomposed the proof of correctness into two parts. The task of the Embedded Verifier is to prove some simple conditions at each run (on-line proof), that have been proved once for all to guarantee the correctness of the translation (off-line proof). We have addressed the problem of the correctness of the implementation of the Embedded Verifier itself by decomposing it into two independent programs, such that only a small kernel of the verifier is critical. }
    @inproceedings{Cimatti:1999rw,
      abstract = {In this paper we describe an industrial project whose goal was the certification of the translator part of a tool used to develop safety critical applications. We have successfully applied a novel formal verification technique.  We have constructed an Embedded Verifier which, for each run of the translator, verifies formally the correctness of the result of each translation, rather than the correctness of the translation algorithm or code. We call this approach Run-time Result Formal Verification. In order to satisfy efficiency requirements on the Embedded Verifier, we have decomposed the proof of correctness into two parts. The task of the Embedded Verifier is to prove some simple conditions at each run (on-line proof), that have been proved once for all to guarantee the correctness of the translation (off-line proof).  We have addressed the problem of the correctness of the implementation of the Embedded Verifier itself by decomposing it into two independent programs, such that only a small kernel of the verifier is critical.  },
      annote = {Publik Printout NOT available},
      author = {Cimatti, Alessandro and Giunchiglia, Fausto and Traverso, Paolo and Villafiorita, Adolfo},
      booktitle = {Proceedings of FLoC99 Workshop on Run-Time Result Verification},
      keywords = {workshop},
      location = {Trento, Italy},
      title = {Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study},
      topics = {industrial_case_study, safety_critical_systems, railways, formal_methods},
      year = {1999}
    }
    
  13. Villafiorita, A. (1995). Reasoning by Analogy via Abstraction. In Proceedings of the Symposium on Abstraction, Reformulation and Approximation, SARA-95 (pp. 156–162). [Abstract] [BibTeX]

    Abstract

    {Abstraction has been used in theorem proving as a heuristic to reduce the search space (see, for instance, [Simpson, 1988]) and as a tool for explanation (see, for instance, [Bundy et al., 1993]). We use abstraction to model certain forms of reasoning by analogy.}
    @inproceedings{Villafiorita:1995la,
      abstract = {Abstraction has been used in theorem proving as a heuristic to reduce the search space (see, for instance, [Simpson, 1988]) and as a tool for explanation (see, for instance, [Bundy et al., 1993]). We use abstraction to model certain forms of reasoning by analogy.},
      annote = {Publik Printout available},
      author = {Villafiorita, Adolfo},
      booktitle = {Proceedings of the Symposium on Abstraction, Reformulation and Approximation, SARA-95},
      keywords = {workshop},
      location = {Ville d’Esterel, Canada},
      month = aug,
      pages = {156–162},
      title = {Reasoning by Analogy via Abstraction},
      topics = {abstraction, theorem_proving, analogical_reasoning, ABSFOL},
      year = {1995}
    }