FormaliSE '13: "Functional SMT Solving with ..."
Functional SMT Solving with Z3 and Racket
Siddharth Agarwal and Amey Karkare
(Facebook, USA; IIT Kanpur, India)
Satisfiability Modulo Theories (SMT) solvers are powerful tools that can quickly solve complex constraints involving Booleans, integers, first-order logic predicates, lists, and other data types. They have a vast number of potential applications, from constraint solving to program analysis and verification. However, they are so complex to use that their power is inaccessible to all but experts in the field. We present an attempt to make using SMT solvers simpler by integrating the Z3 solver into a host language, Racket. The system defines a programmer’s interface in Racket that makes it easy to harness the power of Z3 to discover solutions to logical constraints. The interface, although in Racket, retains the structure and brevity of the SMT-LIB format. This system is expected to be useful for a wide variety of applications, from simple constraint solving to writing tools for debugging, verification, and automatic test generation for functional programs.
@InProceedings{FormaliSE13p15,
author = {Siddharth Agarwal and Amey Karkare},
title = {Functional SMT Solving with Z3 and Racket},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {15--21},
doi = {},
year = {2013},
}
FormaliSE '13: "Recommendations for Improving ..."
Recommendations for Improving the Usability of Formal Methods for Product Lines
Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih, and Pourya Shaker
(University of Waterloo, Canada)
While there may be general agreement on what it means for a formal method to be usable (e.g., ease of modelling, automated and scalable analysis), there is no consensus in the software-engineering or formal-methods communities on what strategies lead to more usable formalisms. In this paper, we aim to raise discussion around such strategies by proposing fourteen concrete recommendations for achieving practical formal methods. Our recommendations apply to research in formal modelling, automated analysis, and automated transformation (e.g., transforming a model into the input to an analysis tool). Our recommendations focus on formal methods for functional requirements of software product lines, as per our experience in this area as part of a research project in collaboration with an automotive manufacturer; however, most of the recommendations apply to formal methods in general. We also provide a brief overview of a formal modelling language and an underdevelopment tool chain that realizes our recommendations.
@InProceedings{FormaliSE13p43,
author = {Joanne M. Atlee and Sandy Beidu and Nancy A. Day and Fathiyeh Faghih and Pourya Shaker},
title = {Recommendations for Improving the Usability of Formal Methods for Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {43--49},
doi = {},
year = {2013},
}
FormaliSE '13: "Recommendations for Improving ..."
Recommendations for Improving the Usability of Formal Methods for Product Lines
Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih, and Pourya Shaker
(University of Waterloo, Canada)
While there may be general agreement on what it means for a formal method to be usable (e.g., ease of modelling, automated and scalable analysis), there is no consensus in the software-engineering or formal-methods communities on what strategies lead to more usable formalisms. In this paper, we aim to raise discussion around such strategies by proposing fourteen concrete recommendations for achieving practical formal methods. Our recommendations apply to research in formal modelling, automated analysis, and automated transformation (e.g., transforming a model into the input to an analysis tool). Our recommendations focus on formal methods for functional requirements of software product lines, as per our experience in this area as part of a research project in collaboration with an automotive manufacturer; however, most of the recommendations apply to formal methods in general. We also provide a brief overview of a formal modelling language and an underdevelopment tool chain that realizes our recommendations.
@InProceedings{FormaliSE13p43,
author = {Joanne M. Atlee and Sandy Beidu and Nancy A. Day and Fathiyeh Faghih and Pourya Shaker},
title = {Recommendations for Improving the Usability of Formal Methods for Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {43--49},
doi = {},
year = {2013},
}
FormaliSE '13: "An Integrated Data Model Verifier ..."
An Integrated Data Model Verifier with Property Templates
Jaideep Nijjar, Ivan Bocic, and Tevfik Bultan
(UC Santa Barbara, USA)
Most modern web applications are built using development frameworks based on the Model-View-Controller (MVC) pattern. In MVC-based web applications the data model specifies the types of objects used by the application and the relations among them. Since the data model forms the foundation of such applications, its correctness is crucial. In this paper we present a tool, iDaVer, that 1) automatically extracts a formal data model specification from applications implemented using the Ruby on Rails framework, 2) provides templates for specifying data model properties, 3) automatically translates the verification of properties specified using these templates to satisfiability queries in three different logics, and 4) uses automated decision procedures and theorem provers to identify which properties are satisfied by the data model, and 5) reports counterexample instances for the properties that fail. Our tool achieves scalable automated verification by exploiting the modularity in the MVC pattern. iDaVer does not require formal specifications to be written manually; thus, our tool enables automated verification and increases the usability by combining automated data model extraction with template-based property specification.
@InProceedings{FormaliSE13p29,
author = {Jaideep Nijjar and Ivan Bocic and Tevfik Bultan},
title = {An Integrated Data Model Verifier with Property Templates},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {29--35},
doi = {},
year = {2013},
}
FormaliSE '13: "Do You Speak Z? Formal Methods ..."
Do You Speak Z? Formal Methods under the Perspective of a Cross-Cultural Adaptation Problem
Andreas Bollin
(University of Klagenfurt, Austria)
The use of formal specifications seems to be a silver bullet in a world where technical systems become more and more software intensive and where quality considerations become increasingly important. However, formal methods and the use of formal specifications are by far not so widespread as they should and could be.
This position paper argues that a broader view onto this situation can be very helpful. It introduces the formal development process as a cross-cultural adaptation problem, discusses pros and cons, and, finally, comes up with a refined model for a formal software development process.
@InProceedings{FormaliSE13p8,
author = {Andreas Bollin},
title = {Do You Speak Z? Formal Methods under the Perspective of a Cross-Cultural Adaptation Problem},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {8--14},
doi = {},
year = {2013},
}
FormaliSE '13: "An Integrated Data Model Verifier ..."
An Integrated Data Model Verifier with Property Templates
Jaideep Nijjar, Ivan Bocic, and Tevfik Bultan
(UC Santa Barbara, USA)
Most modern web applications are built using development frameworks based on the Model-View-Controller (MVC) pattern. In MVC-based web applications the data model specifies the types of objects used by the application and the relations among them. Since the data model forms the foundation of such applications, its correctness is crucial. In this paper we present a tool, iDaVer, that 1) automatically extracts a formal data model specification from applications implemented using the Ruby on Rails framework, 2) provides templates for specifying data model properties, 3) automatically translates the verification of properties specified using these templates to satisfiability queries in three different logics, and 4) uses automated decision procedures and theorem provers to identify which properties are satisfied by the data model, and 5) reports counterexample instances for the properties that fail. Our tool achieves scalable automated verification by exploiting the modularity in the MVC pattern. iDaVer does not require formal specifications to be written manually; thus, our tool enables automated verification and increases the usability by combining automated data model extraction with template-based property specification.
@InProceedings{FormaliSE13p29,
author = {Jaideep Nijjar and Ivan Bocic and Tevfik Bultan},
title = {An Integrated Data Model Verifier with Property Templates},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {29--35},
doi = {},
year = {2013},
}
FormaliSE '13: "A Framework for the Rigorous ..."
A Framework for the Rigorous Design of Highly Adaptive Timed Systems
Maxime Cordy, Axel Legay, Pierre-Yves Schobbens, and Louis-Marie Traonouez
(University of Namur, Belgium; INRIA, France)
Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in response to unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.
@InProceedings{FormaliSE13p64,
author = {Maxime Cordy and Axel Legay and Pierre-Yves Schobbens and Louis-Marie Traonouez},
title = {A Framework for the Rigorous Design of Highly Adaptive Timed Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {64--70},
doi = {},
year = {2013},
}
FormaliSE '13: "Recommendations for Improving ..."
Recommendations for Improving the Usability of Formal Methods for Product Lines
Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih, and Pourya Shaker
(University of Waterloo, Canada)
While there may be general agreement on what it means for a formal method to be usable (e.g., ease of modelling, automated and scalable analysis), there is no consensus in the software-engineering or formal-methods communities on what strategies lead to more usable formalisms. In this paper, we aim to raise discussion around such strategies by proposing fourteen concrete recommendations for achieving practical formal methods. Our recommendations apply to research in formal modelling, automated analysis, and automated transformation (e.g., transforming a model into the input to an analysis tool). Our recommendations focus on formal methods for functional requirements of software product lines, as per our experience in this area as part of a research project in collaboration with an automotive manufacturer; however, most of the recommendations apply to formal methods in general. We also provide a brief overview of a formal modelling language and an underdevelopment tool chain that realizes our recommendations.
@InProceedings{FormaliSE13p43,
author = {Joanne M. Atlee and Sandy Beidu and Nancy A. Day and Fathiyeh Faghih and Pourya Shaker},
title = {Recommendations for Improving the Usability of Formal Methods for Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {43--49},
doi = {},
year = {2013},
}
FormaliSE '13: "Recommendations for Improving ..."
Recommendations for Improving the Usability of Formal Methods for Product Lines
Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih, and Pourya Shaker
(University of Waterloo, Canada)
While there may be general agreement on what it means for a formal method to be usable (e.g., ease of modelling, automated and scalable analysis), there is no consensus in the software-engineering or formal-methods communities on what strategies lead to more usable formalisms. In this paper, we aim to raise discussion around such strategies by proposing fourteen concrete recommendations for achieving practical formal methods. Our recommendations apply to research in formal modelling, automated analysis, and automated transformation (e.g., transforming a model into the input to an analysis tool). Our recommendations focus on formal methods for functional requirements of software product lines, as per our experience in this area as part of a research project in collaboration with an automotive manufacturer; however, most of the recommendations apply to formal methods in general. We also provide a brief overview of a formal modelling language and an underdevelopment tool chain that realizes our recommendations.
@InProceedings{FormaliSE13p43,
author = {Joanne M. Atlee and Sandy Beidu and Nancy A. Day and Fathiyeh Faghih and Pourya Shaker},
title = {Recommendations for Improving the Usability of Formal Methods for Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {43--49},
doi = {},
year = {2013},
}
FormaliSE '13: "Lightweight Formal Models ..."
Lightweight Formal Models of Software Weaknesses
Robin Gandhi, Harvey Siy, and Yan Wu
(University of Nebraska at Omaha, USA)
Many vulnerabilities in today's software products are rehashes of past vulnerabilities. Such rehashes could be a result of software complexity that masks inadvertent loopholes in design and implementation, developer ignorance/disregard for security issues, or use of software in contexts not anticipated for the original specification. While weaknesses and exposures in code are vendor, language, or environment specific, to understand them we need better descriptions that identify their precise characteristics in an unambiguous representation. In this paper, we present a methodology to develop precise and accurate descriptions of common software weaknesses through lightweight formal modeling using Alloy. Natural language descriptions of software weaknesses used for formalization are based on the community developed Common Weakness Enumerations (CWE).
@InProceedings{FormaliSE13p50,
author = {Robin Gandhi and Harvey Siy and Yan Wu},
title = {Lightweight Formal Models of Software Weaknesses},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {50--56},
doi = {},
year = {2013},
}
FormaliSE '13: "Automatic Validation of Infinite ..."
Automatic Validation of Infinite Real-Time Systems
Thomas Göthel and Sabine Glesner
(TU Berlin, Germany)
In safety-critical areas, complete and machine-assisted verification techniques for infinite real-time systems are required to ensure their correctness in all cases and to cope with their complexity. Previously, we presented a theorem prover-based comprehensive and compositional verification approach using the Timed CSP process calculus to model and verify possibly infinite real-time systems. However, it lacks support for employing automatic verification approaches to validate finite sub-processes of the overall system model. This mainly comes from insufficient automatic verification support for finite Timed CSP processes. In this paper, we present a real-time logic and a transformation of the Timed CSP process calculus to UPPAAL timed automata. We discuss their integration into our comprehensive verification approach as part of a prior validation phase. This is crucial because the effort for interactive verification in the theorem prover is thereby reduced considerably. By this, we provide a comprehensive machine-assisted verification approach without losing the benefits of automatic verification.
@InProceedings{FormaliSE13p57,
author = {Thomas Göthel and Sabine Glesner},
title = {Automatic Validation of Infinite Real-Time Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {57--63},
doi = {},
year = {2013},
}
FormaliSE '13: "Towards a Formalism-Based ..."
Towards a Formalism-Based Toolkit for Automotive Applications
Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson, and Manuel Mazzara
(Bosch, Germany; Newcastle University, UK)
The success of a number of projects has been shown to be significantly improved by the use of a formalism . However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a step- wise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.
@InProceedings{FormaliSE13p36,
author = {Rainer Gmehlich and Katrin Grau and Felix Loesch and Alexei Iliasov and Michael Jackson and Manuel Mazzara},
title = {Towards a Formalism-Based Toolkit for Automotive Applications},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {36--42},
doi = {},
year = {2013},
}
FormaliSE '13: "Automatic Validation of Infinite ..."
Automatic Validation of Infinite Real-Time Systems
Thomas Göthel and Sabine Glesner
(TU Berlin, Germany)
In safety-critical areas, complete and machine-assisted verification techniques for infinite real-time systems are required to ensure their correctness in all cases and to cope with their complexity. Previously, we presented a theorem prover-based comprehensive and compositional verification approach using the Timed CSP process calculus to model and verify possibly infinite real-time systems. However, it lacks support for employing automatic verification approaches to validate finite sub-processes of the overall system model. This mainly comes from insufficient automatic verification support for finite Timed CSP processes. In this paper, we present a real-time logic and a transformation of the Timed CSP process calculus to UPPAAL timed automata. We discuss their integration into our comprehensive verification approach as part of a prior validation phase. This is crucial because the effort for interactive verification in the theorem prover is thereby reduced considerably. By this, we provide a comprehensive machine-assisted verification approach without losing the benefits of automatic verification.
@InProceedings{FormaliSE13p57,
author = {Thomas Göthel and Sabine Glesner},
title = {Automatic Validation of Infinite Real-Time Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {57--63},
doi = {},
year = {2013},
}
FormaliSE '13: "Towards a Formalism-Based ..."
Towards a Formalism-Based Toolkit for Automotive Applications
Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson, and Manuel Mazzara
(Bosch, Germany; Newcastle University, UK)
The success of a number of projects has been shown to be significantly improved by the use of a formalism . However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a step- wise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.
@InProceedings{FormaliSE13p36,
author = {Rainer Gmehlich and Katrin Grau and Felix Loesch and Alexei Iliasov and Michael Jackson and Manuel Mazzara},
title = {Towards a Formalism-Based Toolkit for Automotive Applications},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {36--42},
doi = {},
year = {2013},
}
FormaliSE '13: "Towards a Formalism-Based ..."
Towards a Formalism-Based Toolkit for Automotive Applications
Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson, and Manuel Mazzara
(Bosch, Germany; Newcastle University, UK)
The success of a number of projects has been shown to be significantly improved by the use of a formalism . However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a step- wise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.
@InProceedings{FormaliSE13p36,
author = {Rainer Gmehlich and Katrin Grau and Felix Loesch and Alexei Iliasov and Michael Jackson and Manuel Mazzara},
title = {Towards a Formalism-Based Toolkit for Automotive Applications},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {36--42},
doi = {},
year = {2013},
}
FormaliSE '13: "Towards a Formalism-Based ..."
Towards a Formalism-Based Toolkit for Automotive Applications
Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson, and Manuel Mazzara
(Bosch, Germany; Newcastle University, UK)
The success of a number of projects has been shown to be significantly improved by the use of a formalism . However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a step- wise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.
@InProceedings{FormaliSE13p36,
author = {Rainer Gmehlich and Katrin Grau and Felix Loesch and Alexei Iliasov and Michael Jackson and Manuel Mazzara},
title = {Towards a Formalism-Based Toolkit for Automotive Applications},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {36--42},
doi = {},
year = {2013},
}
FormaliSE '13: "Functional SMT Solving with ..."
Functional SMT Solving with Z3 and Racket
Siddharth Agarwal and Amey Karkare
(Facebook, USA; IIT Kanpur, India)
Satisfiability Modulo Theories (SMT) solvers are powerful tools that can quickly solve complex constraints involving Booleans, integers, first-order logic predicates, lists, and other data types. They have a vast number of potential applications, from constraint solving to program analysis and verification. However, they are so complex to use that their power is inaccessible to all but experts in the field. We present an attempt to make using SMT solvers simpler by integrating the Z3 solver into a host language, Racket. The system defines a programmer’s interface in Racket that makes it easy to harness the power of Z3 to discover solutions to logical constraints. The interface, although in Racket, retains the structure and brevity of the SMT-LIB format. This system is expected to be useful for a wide variety of applications, from simple constraint solving to writing tools for debugging, verification, and automatic test generation for functional programs.
@InProceedings{FormaliSE13p15,
author = {Siddharth Agarwal and Amey Karkare},
title = {Functional SMT Solving with Z3 and Racket},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {15--21},
doi = {},
year = {2013},
}
FormaliSE '13: "A Framework for the Rigorous ..."
A Framework for the Rigorous Design of Highly Adaptive Timed Systems
Maxime Cordy, Axel Legay, Pierre-Yves Schobbens, and Louis-Marie Traonouez
(University of Namur, Belgium; INRIA, France)
Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in response to unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.
@InProceedings{FormaliSE13p64,
author = {Maxime Cordy and Axel Legay and Pierre-Yves Schobbens and Louis-Marie Traonouez},
title = {A Framework for the Rigorous Design of Highly Adaptive Timed Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {64--70},
doi = {},
year = {2013},
}
FormaliSE '13: "Towards a Formalism-Based ..."
Towards a Formalism-Based Toolkit for Automotive Applications
Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson, and Manuel Mazzara
(Bosch, Germany; Newcastle University, UK)
The success of a number of projects has been shown to be significantly improved by the use of a formalism . However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a step- wise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.
@InProceedings{FormaliSE13p36,
author = {Rainer Gmehlich and Katrin Grau and Felix Loesch and Alexei Iliasov and Michael Jackson and Manuel Mazzara},
title = {Towards a Formalism-Based Toolkit for Automotive Applications},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {36--42},
doi = {},
year = {2013},
}
FormaliSE '13: "Trace Based Reachability Verification ..."
Trace Based Reachability Verification for Statecharts
Kumar Madhukar, Ravindra Metta, Ulka Shrotri, and R. Venkatesh
(Tata Consultancy Services, India)
Statecharts are widely used to model the behavior of reactive systems. While this visual formalism makes modeling easier, the state of the art in verification of statechart specifications is far from satisfactory due to the state explosion problem. We present History Abstraction, a trace-based verification technique to address this problem. Given a set of traces in a statechart model, the model is abstracted to contain at most three states per statechart: current, history and future. A path to a desired state in the abstract model is a sketch of a potential path to that state in the original model. We follow an incremental concretization procedure to extend the sketch to a complete path in the original model. This paper presents our technique. Our experiments suggest that the technique scales to large industry models.
@InProceedings{FormaliSE13p22,
author = {Kumar Madhukar and Ravindra Metta and Ulka Shrotri and R. Venkatesh},
title = {Trace Based Reachability Verification for Statecharts},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {22--28},
doi = {},
year = {2013},
}
FormaliSE '13: "Towards a Formalism-Based ..."
Towards a Formalism-Based Toolkit for Automotive Applications
Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson, and Manuel Mazzara
(Bosch, Germany; Newcastle University, UK)
The success of a number of projects has been shown to be significantly improved by the use of a formalism . However, there remains an open issue: to what extent can a development process based on a singular formal notation and method succeed. The majority of approaches demonstrate a low level of flexibility by attempting to use a single notation to express all of the different aspects encountered in software development. Often, these approaches leave a number of scalability issues open. We prefer a more eclectic approach. In our experience, the use of a formalism-based toolkit with adequate notations for each development phase is a viable solution. Following this principle, any specific notation is used only where and when it is really suitable and not necessarily over the entire software lifecycle. The approach explored in this article is perhaps slowly emerging in practice we hope to accelerate its adoption. However, the major challenge is still finding the best way to instantiate it for each specific application scenario. In this work, we describe a development process and method for automotive applications which consists of five phases. The process recognizes the need for having adequate (and tailored) notations (Problem Frames, Requirements State Machine Language, and Event-B) for each development phase as well as direct traceability between the documents produced during each phase. This allows for a step- wise verification/validation of the system under development. The ideas for the formal development method have evolved over two significant case studies carried out in the DEPLOY project.
@InProceedings{FormaliSE13p36,
author = {Rainer Gmehlich and Katrin Grau and Felix Loesch and Alexei Iliasov and Michael Jackson and Manuel Mazzara},
title = {Towards a Formalism-Based Toolkit for Automotive Applications},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {36--42},
doi = {},
year = {2013},
}
FormaliSE '13: "Trace Based Reachability Verification ..."
Trace Based Reachability Verification for Statecharts
Kumar Madhukar, Ravindra Metta, Ulka Shrotri, and R. Venkatesh
(Tata Consultancy Services, India)
Statecharts are widely used to model the behavior of reactive systems. While this visual formalism makes modeling easier, the state of the art in verification of statechart specifications is far from satisfactory due to the state explosion problem. We present History Abstraction, a trace-based verification technique to address this problem. Given a set of traces in a statechart model, the model is abstracted to contain at most three states per statechart: current, history and future. A path to a desired state in the abstract model is a sketch of a potential path to that state in the original model. We follow an incremental concretization procedure to extend the sketch to a complete path in the original model. This paper presents our technique. Our experiments suggest that the technique scales to large industry models.
@InProceedings{FormaliSE13p22,
author = {Kumar Madhukar and Ravindra Metta and Ulka Shrotri and R. Venkatesh},
title = {Trace Based Reachability Verification for Statecharts},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {22--28},
doi = {},
year = {2013},
}
FormaliSE '13: "An Integrated Data Model Verifier ..."
An Integrated Data Model Verifier with Property Templates
Jaideep Nijjar, Ivan Bocic, and Tevfik Bultan
(UC Santa Barbara, USA)
Most modern web applications are built using development frameworks based on the Model-View-Controller (MVC) pattern. In MVC-based web applications the data model specifies the types of objects used by the application and the relations among them. Since the data model forms the foundation of such applications, its correctness is crucial. In this paper we present a tool, iDaVer, that 1) automatically extracts a formal data model specification from applications implemented using the Ruby on Rails framework, 2) provides templates for specifying data model properties, 3) automatically translates the verification of properties specified using these templates to satisfiability queries in three different logics, and 4) uses automated decision procedures and theorem provers to identify which properties are satisfied by the data model, and 5) reports counterexample instances for the properties that fail. Our tool achieves scalable automated verification by exploiting the modularity in the MVC pattern. iDaVer does not require formal specifications to be written manually; thus, our tool enables automated verification and increases the usability by combining automated data model extraction with template-based property specification.
@InProceedings{FormaliSE13p29,
author = {Jaideep Nijjar and Ivan Bocic and Tevfik Bultan},
title = {An Integrated Data Model Verifier with Property Templates},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {29--35},
doi = {},
year = {2013},
}
FormaliSE '13: "A Framework for the Rigorous ..."
A Framework for the Rigorous Design of Highly Adaptive Timed Systems
Maxime Cordy, Axel Legay, Pierre-Yves Schobbens, and Louis-Marie Traonouez
(University of Namur, Belgium; INRIA, France)
Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in response to unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.
@InProceedings{FormaliSE13p64,
author = {Maxime Cordy and Axel Legay and Pierre-Yves Schobbens and Louis-Marie Traonouez},
title = {A Framework for the Rigorous Design of Highly Adaptive Timed Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {64--70},
doi = {},
year = {2013},
}
FormaliSE '13: "Recommendations for Improving ..."
Recommendations for Improving the Usability of Formal Methods for Product Lines
Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih, and Pourya Shaker
(University of Waterloo, Canada)
While there may be general agreement on what it means for a formal method to be usable (e.g., ease of modelling, automated and scalable analysis), there is no consensus in the software-engineering or formal-methods communities on what strategies lead to more usable formalisms. In this paper, we aim to raise discussion around such strategies by proposing fourteen concrete recommendations for achieving practical formal methods. Our recommendations apply to research in formal modelling, automated analysis, and automated transformation (e.g., transforming a model into the input to an analysis tool). Our recommendations focus on formal methods for functional requirements of software product lines, as per our experience in this area as part of a research project in collaboration with an automotive manufacturer; however, most of the recommendations apply to formal methods in general. We also provide a brief overview of a formal modelling language and an underdevelopment tool chain that realizes our recommendations.
@InProceedings{FormaliSE13p43,
author = {Joanne M. Atlee and Sandy Beidu and Nancy A. Day and Fathiyeh Faghih and Pourya Shaker},
title = {Recommendations for Improving the Usability of Formal Methods for Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {43--49},
doi = {},
year = {2013},
}
FormaliSE '13: "Trace Based Reachability Verification ..."
Trace Based Reachability Verification for Statecharts
Kumar Madhukar, Ravindra Metta, Ulka Shrotri, and R. Venkatesh
(Tata Consultancy Services, India)
Statecharts are widely used to model the behavior of reactive systems. While this visual formalism makes modeling easier, the state of the art in verification of statechart specifications is far from satisfactory due to the state explosion problem. We present History Abstraction, a trace-based verification technique to address this problem. Given a set of traces in a statechart model, the model is abstracted to contain at most three states per statechart: current, history and future. A path to a desired state in the abstract model is a sketch of a potential path to that state in the original model. We follow an incremental concretization procedure to extend the sketch to a complete path in the original model. This paper presents our technique. Our experiments suggest that the technique scales to large industry models.
@InProceedings{FormaliSE13p22,
author = {Kumar Madhukar and Ravindra Metta and Ulka Shrotri and R. Venkatesh},
title = {Trace Based Reachability Verification for Statecharts},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {22--28},
doi = {},
year = {2013},
}
FormaliSE '13: "Lightweight Formal Models ..."
Lightweight Formal Models of Software Weaknesses
Robin Gandhi, Harvey Siy, and Yan Wu
(University of Nebraska at Omaha, USA)
Many vulnerabilities in today's software products are rehashes of past vulnerabilities. Such rehashes could be a result of software complexity that masks inadvertent loopholes in design and implementation, developer ignorance/disregard for security issues, or use of software in contexts not anticipated for the original specification. While weaknesses and exposures in code are vendor, language, or environment specific, to understand them we need better descriptions that identify their precise characteristics in an unambiguous representation. In this paper, we present a methodology to develop precise and accurate descriptions of common software weaknesses through lightweight formal modeling using Alloy. Natural language descriptions of software weaknesses used for formalization are based on the community developed Common Weakness Enumerations (CWE).
@InProceedings{FormaliSE13p50,
author = {Robin Gandhi and Harvey Siy and Yan Wu},
title = {Lightweight Formal Models of Software Weaknesses},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {50--56},
doi = {},
year = {2013},
}
FormaliSE '13: "A Framework for the Rigorous ..."
A Framework for the Rigorous Design of Highly Adaptive Timed Systems
Maxime Cordy, Axel Legay, Pierre-Yves Schobbens, and Louis-Marie Traonouez
(University of Namur, Belgium; INRIA, France)
Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in response to unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.
@InProceedings{FormaliSE13p64,
author = {Maxime Cordy and Axel Legay and Pierre-Yves Schobbens and Louis-Marie Traonouez},
title = {A Framework for the Rigorous Design of Highly Adaptive Timed Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {64--70},
doi = {},
year = {2013},
}
FormaliSE '13: "Trace Based Reachability Verification ..."
Trace Based Reachability Verification for Statecharts
Kumar Madhukar, Ravindra Metta, Ulka Shrotri, and R. Venkatesh
(Tata Consultancy Services, India)
Statecharts are widely used to model the behavior of reactive systems. While this visual formalism makes modeling easier, the state of the art in verification of statechart specifications is far from satisfactory due to the state explosion problem. We present History Abstraction, a trace-based verification technique to address this problem. Given a set of traces in a statechart model, the model is abstracted to contain at most three states per statechart: current, history and future. A path to a desired state in the abstract model is a sketch of a potential path to that state in the original model. We follow an incremental concretization procedure to extend the sketch to a complete path in the original model. This paper presents our technique. Our experiments suggest that the technique scales to large industry models.
@InProceedings{FormaliSE13p22,
author = {Kumar Madhukar and Ravindra Metta and Ulka Shrotri and R. Venkatesh},
title = {Trace Based Reachability Verification for Statecharts},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {22--28},
doi = {},
year = {2013},
}
FormaliSE '13: "Though This Be Madness, Yet ..."
Though This Be Madness, Yet There Is Method in It? (Keynote)
Alan Wassyng
(McMaster University, Canada)
After decades of research, and despite significant advancement, formal methods are still not widely used in industrial software development. Industry practitioners believe that the methods and tools coming out of academia are, to a large extent, irrelevant and ineffective in tackling real-life projects. They are difficult to use, esoteric, and do not scale (at all). This paper reflects more than twenty years spent in first experiencing the problems in industry, and then struggling to do something about it in academia. We present some examples of formal method madness/blindness, as well as a few successes. We believe the problem is deep. To start to address it and make progress in producing methods that are truly usable in industry, and rigorous enough to make them effective engineering methods, we need to reconsider the role of computer scientists, software engineers, software developers, as well as the hurdles to promotion for academics. Along the way, the paper will present a few fundamental principles that we think spell the difference between success and failure in producing usable formal methods, and convincing software professionals in industry to adopt them.
@InProceedings{FormaliSE13p1,
author = {Alan Wassyng},
title = {Though This Be Madness, Yet There Is Method in It? (Keynote)},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {1--7},
doi = {},
year = {2013},
}
FormaliSE '13: "Lightweight Formal Models ..."
Lightweight Formal Models of Software Weaknesses
Robin Gandhi, Harvey Siy, and Yan Wu
(University of Nebraska at Omaha, USA)
Many vulnerabilities in today's software products are rehashes of past vulnerabilities. Such rehashes could be a result of software complexity that masks inadvertent loopholes in design and implementation, developer ignorance/disregard for security issues, or use of software in contexts not anticipated for the original specification. While weaknesses and exposures in code are vendor, language, or environment specific, to understand them we need better descriptions that identify their precise characteristics in an unambiguous representation. In this paper, we present a methodology to develop precise and accurate descriptions of common software weaknesses through lightweight formal modeling using Alloy. Natural language descriptions of software weaknesses used for formalization are based on the community developed Common Weakness Enumerations (CWE).
@InProceedings{FormaliSE13p50,
author = {Robin Gandhi and Harvey Siy and Yan Wu},
title = {Lightweight Formal Models of Software Weaknesses},
booktitle = {Proc.\ FormaliSE},
publisher = {IEEE},
pages = {50--56},
doi = {},
year = {2013},
}