Workshop FormaliSE 2014 – Author Index |
Contents -
Abstracts -
Authors
|
| Agrawal, Akshay |
FormaliSE '14: "Formalization of Software ..."
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits (Vanderbilt University, USA) The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach. 
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
|
|
| Araki, Keijiro |
FormaliSE '14: "Generating Supportive Hypotheses ..."
Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model
Shigeru Kusakabe, Hsin-Hung Lin, Yoichi Omori, and Keijiro Araki (Kyushu University, Japan) We are investigating the effective facilitation methodology for the introduction of formal methods into actual software developments. One of the important issues is how to define and develop an adequate development process with formal methods. In this paper, we discuss this issue from a view point of software process improvement using a standard development process model, CMMI-DEV, which is a compilation of best practices in software development. We expect using the standard process model as a reference can facilitate common understanding for the advantages of formal methods and the comparison between actual instances of software process with formal methods. This approach leads to the exploitation of knowledge and findings obtained in the successful cases. We generate supportive hypotheses in the effect of formal methods on software development processes by using the standard improvement model. Then, we weakly examine them with a combination of a small-scale process, which has a strong relation to the organization level process, and a model-oriented formal method, VDM.
@InProceedings{FormaliSE14p24,
author = {Shigeru Kusakabe and Hsin-Hung Lin and Yoichi Omori and Keijiro Araki},
title = {Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {24--30},
doi = {},
year = {2014},
}
|
|
| Baresi, Luciano |
FormaliSE '14: "Flexible Modular Formalization ..."
Flexible Modular Formalization of UML Sequence Diagrams
Luciano Baresi, Mohammad Mehdi Pourhashem Kallehbasti, and Matteo Rossi (Politecnico di Milano, Italy) UML Sequence Diagrams are one of the most commonly used type of UML diagrams in practice. Their semantics is often considered to be straightforward, but a more detailed analysis reveals diverse interpretations. These different choices must be properly supported by verification tools. This paper describes a formal framework for capturing semantic choices in a precise and modular way. The user is then able to select the semantics of interest, mix different interpretations, and analyze diagrams according to the chosen solution. This solution is supported by Corretto, our UML verification environment, to allow the user to play with different semantics and prove properties on Sequence Diagrams, accordingly.
@InProceedings{FormaliSE14p10,
author = {Luciano Baresi and Mohammad Mehdi Pourhashem Kallehbasti and Matteo Rossi},
title = {Flexible Modular Formalization of UML Sequence Diagrams},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {10--16},
doi = {},
year = {2014},
}
|
|
| Beek, Maurice H. ter |
FormaliSE '14: "Using mCRL2 for the Analysis ..."
Using mCRL2 for the Analysis of Software Product Lines
Maurice H. ter Beek and Erik P. de Vink (ISTI-CNR, Italy; Eindhoven University of Technology, Netherlands; CWI, Netherlands) We show how the formal specification language mCRL2 and its state-of-the-art toolset can be used successfully to model and analyze variability in software product lines. The mCRL2 toolset supports parametrized modeling, model reduction and quality assurance techniques like model checking. We present a proof-of-concept, which moreover illustrates the use of data in mCRL2 and also how to exploit its data language to manage feature attributes of software product lines and quantitative constraints between attributes and features.
@InProceedings{FormaliSE14p31,
author = {Maurice H. ter Beek and Erik P. de Vink},
title = {Using mCRL2 for the Analysis of Software Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {31--37},
doi = {},
year = {2014},
}
|
|
| Bhiri, Mohamed Tahar |
FormaliSE '14: "From an Abstract Specification ..."
From an Abstract Specification in Event-B toward an UML/OCL Model
Imen Sayar and Mohamed Tahar Bhiri (University of Sfax, Tunisia; University of Lorraine, France) The formal approach of software development promotes getting proved correct software. It faces the shortcomings of the classical approach concerning the ambiguity of the requirements document, the risk of errors distributed to all phases and the high testing cost (because of late detection of such errors). However, this approach poses problems mainly related to the participation of various actors not necessarily professionals in formal methods, maintenance and especially the development of an "optimal" refinement strategy. To overcome the limitations of these two approaches, we propose a hybrid approach that combines the formal approach (Event-B) and the classical approach (UML/OCL). Upstream phases of our approach include: Rewriting the requirements document, Refinement strategy, Abstract specification, Horizontal refinement and Validation. Downstream phases contain the Construction of a UML/EM-OCL model, Refinement, Integration of design and implementation decisions, Coding and Integration. In this paper, we show the feasibility of our approach on a case study: An Electronic Hotel Key System (SCEH). The problem of transition from formal (Event-B) to the semi-formal (UML/OCL) is processed by our OCL extension called EM-OCL.
@InProceedings{FormaliSE14p17,
author = {Imen Sayar and Mohamed Tahar Bhiri},
title = {From an Abstract Specification in Event-B toward an UML/OCL Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {17--23},
doi = {},
year = {2014},
}
|
|
| Biatek, Jason |
FormaliSE '14: "Analysis and Testing of PLEXIL ..."
Analysis and Testing of PLEXIL Plans
Jason Biatek, Michael W. Whalen, Mats P. E. Heimdahl, Sanjai Rayadurgam, and Michael R. Lowry (University of Minnesota, USA; NASA Ames Research Center, USA) Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.
@InProceedings{FormaliSE14p52,
author = {Jason Biatek and Michael W. Whalen and Mats P. E. Heimdahl and Sanjai Rayadurgam and Michael R. Lowry},
title = {Analysis and Testing of PLEXIL Plans},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {52--58},
doi = {},
year = {2014},
}
|
|
| Bollin, Andreas |
FormaliSE '14: "Formal Specification Comprehension: ..."
Formal Specification Comprehension: The Art of Reading and Writing Z
Andreas Bollin and Dominik Rauner-Reithmayer (University of Klagenfurt, Austria; Carinthia University of Applied Sciences, Austria) Formal Methods have been developed to provide systematic and rigorous techniques for software development. They found their place in document-driven development processes as well as in the agile world. However, reading, understanding and working with a formal specification still turns out to be a real challenge. This paper tries to identify the underlying cause and argues that comprehensibility of a specification is one of the key factors. It presents some first findings of an extensive study investigating the readability of Z specifications and comes up with a set of recommendations in writing formal specifications so that the syntactic gap between the mathematics and the natural language requirements description can be bridged more easily.
@InProceedings{FormaliSE14p3,
author = {Andreas Bollin and Dominik Rauner-Reithmayer},
title = {Formal Specification Comprehension: The Art of Reading and Writing Z},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {3--9},
doi = {},
year = {2014},
}
|
|
| De Vink, Erik P. |
FormaliSE '14: "Using mCRL2 for the Analysis ..."
Using mCRL2 for the Analysis of Software Product Lines
Maurice H. ter Beek and Erik P. de Vink (ISTI-CNR, Italy; Eindhoven University of Technology, Netherlands; CWI, Netherlands) We show how the formal specification language mCRL2 and its state-of-the-art toolset can be used successfully to model and analyze variability in software product lines. The mCRL2 toolset supports parametrized modeling, model reduction and quality assurance techniques like model checking. We present a proof-of-concept, which moreover illustrates the use of data in mCRL2 and also how to exploit its data language to manage feature attributes of software product lines and quantitative constraints between attributes and features.
@InProceedings{FormaliSE14p31,
author = {Maurice H. ter Beek and Erik P. de Vink},
title = {Using mCRL2 for the Analysis of Software Product Lines},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {31--37},
doi = {},
year = {2014},
}
|
|
| Heimdahl, Mats P. E. |
FormaliSE '14: "Analysis and Testing of PLEXIL ..."
Analysis and Testing of PLEXIL Plans
Jason Biatek, Michael W. Whalen, Mats P. E. Heimdahl, Sanjai Rayadurgam, and Michael R. Lowry (University of Minnesota, USA; NASA Ames Research Center, USA) Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.
@InProceedings{FormaliSE14p52,
author = {Jason Biatek and Michael W. Whalen and Mats P. E. Heimdahl and Sanjai Rayadurgam and Michael R. Lowry},
title = {Analysis and Testing of PLEXIL Plans},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {52--58},
doi = {},
year = {2014},
}
|
|
| Kusakabe, Shigeru |
FormaliSE '14: "Generating Supportive Hypotheses ..."
Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model
Shigeru Kusakabe, Hsin-Hung Lin, Yoichi Omori, and Keijiro Araki (Kyushu University, Japan) We are investigating the effective facilitation methodology for the introduction of formal methods into actual software developments. One of the important issues is how to define and develop an adequate development process with formal methods. In this paper, we discuss this issue from a view point of software process improvement using a standard development process model, CMMI-DEV, which is a compilation of best practices in software development. We expect using the standard process model as a reference can facilitate common understanding for the advantages of formal methods and the comparison between actual instances of software process with formal methods. This approach leads to the exploitation of knowledge and findings obtained in the successful cases. We generate supportive hypotheses in the effect of formal methods on software development processes by using the standard improvement model. Then, we weakly examine them with a combination of a small-scale process, which has a strong relation to the organization level process, and a model-oriented formal method, VDM.
@InProceedings{FormaliSE14p24,
author = {Shigeru Kusakabe and Hsin-Hung Lin and Yoichi Omori and Keijiro Araki},
title = {Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {24--30},
doi = {},
year = {2014},
}
|
|
| Levendovszky, Tihamer |
FormaliSE '14: "Formalization of Software ..."
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits (Vanderbilt University, USA) The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach.
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
|
|
| Lin, Hsin-Hung |
FormaliSE '14: "Generating Supportive Hypotheses ..."
Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model
Shigeru Kusakabe, Hsin-Hung Lin, Yoichi Omori, and Keijiro Araki (Kyushu University, Japan) We are investigating the effective facilitation methodology for the introduction of formal methods into actual software developments. One of the important issues is how to define and develop an adequate development process with formal methods. In this paper, we discuss this issue from a view point of software process improvement using a standard development process model, CMMI-DEV, which is a compilation of best practices in software development. We expect using the standard process model as a reference can facilitate common understanding for the advantages of formal methods and the comparison between actual instances of software process with formal methods. This approach leads to the exploitation of knowledge and findings obtained in the successful cases. We generate supportive hypotheses in the effect of formal methods on software development processes by using the standard improvement model. Then, we weakly examine them with a combination of a small-scale process, which has a strong relation to the organization level process, and a model-oriented formal method, VDM.
@InProceedings{FormaliSE14p24,
author = {Shigeru Kusakabe and Hsin-Hung Lin and Yoichi Omori and Keijiro Araki},
title = {Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {24--30},
doi = {},
year = {2014},
}
|
|
| Lowry, Michael R. |
FormaliSE '14: "Analysis and Testing of PLEXIL ..."
Analysis and Testing of PLEXIL Plans
Jason Biatek, Michael W. Whalen, Mats P. E. Heimdahl, Sanjai Rayadurgam, and Michael R. Lowry (University of Minnesota, USA; NASA Ames Research Center, USA) Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.
@InProceedings{FormaliSE14p52,
author = {Jason Biatek and Michael W. Whalen and Mats P. E. Heimdahl and Sanjai Rayadurgam and Michael R. Lowry},
title = {Analysis and Testing of PLEXIL Plans},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {52--58},
doi = {},
year = {2014},
}
|
|
| Nanjundappa, Mahesh |
FormaliSE '14: "Compiling Polychronous Programs ..."
Compiling Polychronous Programs into Conditional Partial Orders for ASIP Synthesis
Mahesh Nanjundappa and Sandeep K. Shukla (Virginia Tech, USA) Synthesis of application specific hardware which minimizes area while not sacrificing latency or clock speed is a much researched problem. In most of the past works, the hardware is described structurally in hardware description languages with behaviors attached to structures. Since the structure is manually decided, the architect has to decide whether certain components can be reused without increasing latency. For example, if one can prove that certain behaviors never happen at the same time, these behaviors can be mapped to common components, with a simple control state machine determining which behavioral mode the behavior belongs to. Since application specific hardware are used as co-processors for performance boost, and such computations are best described as a data-flow computation (such as signal processing, encryption etc.,), we choose a high level data-flow oriented formal specification language, and use a new semantic model for this specification language, namely conditional partial order graphs. The advantage of our approach is that our specification language MRICDF is graphical, polychronous, has formal semantics, and hence synthesizing its control structure into conditional partial order is a natural fit. Additionally, the specific calculus of constraints in polychronous languages -- namely clock calculus, and associated analysis with Boolean theory of prime implicates, and constraint satisfiability checking with SMT solvers provide us with a natural way of discovering behaviors that belong to disjoint modes, and thereby allow us to reuse components with simple micro-instruction set synthesis. In this paper, we show how MRICDF can be used to formally synthesize such application specific instruction processors. Past approaches to synthesize hardware from the polychronous language SIGNAL were focused on synthesizing logic with hierarchical conditional dependency graphs as internal representation. Unlike those, we are synthesizing an application specific instruction set processor by automated synthesis of control and scheduling data-path.
@InProceedings{FormaliSE14p38,
author = {Mahesh Nanjundappa and Sandeep K. Shukla},
title = {Compiling Polychronous Programs into Conditional Partial Orders for ASIP Synthesis},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {38--44},
doi = {},
year = {2014},
}
|
|
| Neema, Sandeep |
FormaliSE '14: "Formalization of Software ..."
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits (Vanderbilt University, USA) The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach.
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
|
|
| Nori, Aditya V. |
FormaliSE '14: "Software Reliability via Machine ..."
Software Reliability via Machine Learning (Invited Talk)
Aditya V. Nori (Microsoft Research, India) Computing good invariants is key to effective and efficient program verification. In this talk I will describe our experiences in using machine learning techniques (support vector machines, linear regression) for computing invariants useful for program verification as well as for fine tuning verification tools.
@InProceedings{FormaliSE14p1,
author = {Aditya V. Nori},
title = {Software Reliability via Machine Learning (Invited Talk)},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {1--2},
doi = {},
year = {2014},
}
|
|
| Omori, Yoichi |
FormaliSE '14: "Generating Supportive Hypotheses ..."
Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model
Shigeru Kusakabe, Hsin-Hung Lin, Yoichi Omori, and Keijiro Araki (Kyushu University, Japan) We are investigating the effective facilitation methodology for the introduction of formal methods into actual software developments. One of the important issues is how to define and develop an adequate development process with formal methods. In this paper, we discuss this issue from a view point of software process improvement using a standard development process model, CMMI-DEV, which is a compilation of best practices in software development. We expect using the standard process model as a reference can facilitate common understanding for the advantages of formal methods and the comparison between actual instances of software process with formal methods. This approach leads to the exploitation of knowledge and findings obtained in the successful cases. We generate supportive hypotheses in the effect of formal methods on software development processes by using the standard improvement model. Then, we weakly examine them with a combination of a small-scale process, which has a strong relation to the organization level process, and a model-oriented formal method, VDM.
@InProceedings{FormaliSE14p24,
author = {Shigeru Kusakabe and Hsin-Hung Lin and Yoichi Omori and Keijiro Araki},
title = {Generating Supportive Hypotheses in Introducing Formal Methods using a Software Processes Improvement Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {24--30},
doi = {},
year = {2014},
}
|
|
| Porter, Joseph |
FormaliSE '14: "Formalization of Software ..."
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits (Vanderbilt University, USA) The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach.
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
|
|
| Pourhashem Kallehbasti, Mohammad Mehdi |
FormaliSE '14: "Flexible Modular Formalization ..."
Flexible Modular Formalization of UML Sequence Diagrams
Luciano Baresi, Mohammad Mehdi Pourhashem Kallehbasti, and Matteo Rossi (Politecnico di Milano, Italy) UML Sequence Diagrams are one of the most commonly used type of UML diagrams in practice. Their semantics is often considered to be straightforward, but a more detailed analysis reveals diverse interpretations. These different choices must be properly supported by verification tools. This paper describes a formal framework for capturing semantic choices in a precise and modular way. The user is then able to select the semantics of interest, mix different interpretations, and analyze diagrams according to the chosen solution. This solution is supported by Corretto, our UML verification environment, to allow the user to play with different semantics and prove properties on Sequence Diagrams, accordingly.
@InProceedings{FormaliSE14p10,
author = {Luciano Baresi and Mohammad Mehdi Pourhashem Kallehbasti and Matteo Rossi},
title = {Flexible Modular Formalization of UML Sequence Diagrams},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {10--16},
doi = {},
year = {2014},
}
|
|
| Rauner-Reithmayer, Dominik |
FormaliSE '14: "Formal Specification Comprehension: ..."
Formal Specification Comprehension: The Art of Reading and Writing Z
Andreas Bollin and Dominik Rauner-Reithmayer (University of Klagenfurt, Austria; Carinthia University of Applied Sciences, Austria) Formal Methods have been developed to provide systematic and rigorous techniques for software development. They found their place in document-driven development processes as well as in the agile world. However, reading, understanding and working with a formal specification still turns out to be a real challenge. This paper tries to identify the underlying cause and argues that comprehensibility of a specification is one of the key factors. It presents some first findings of an extensive study investigating the readability of Z specifications and comes up with a set of recommendations in writing formal specifications so that the syntactic gap between the mathematics and the natural language requirements description can be bridged more easily.
@InProceedings{FormaliSE14p3,
author = {Andreas Bollin and Dominik Rauner-Reithmayer},
title = {Formal Specification Comprehension: The Art of Reading and Writing Z},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {3--9},
doi = {},
year = {2014},
}
|
|
| Rayadurgam, Sanjai |
FormaliSE '14: "Analysis and Testing of PLEXIL ..."
Analysis and Testing of PLEXIL Plans
Jason Biatek, Michael W. Whalen, Mats P. E. Heimdahl, Sanjai Rayadurgam, and Michael R. Lowry (University of Minnesota, USA; NASA Ames Research Center, USA) Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.
@InProceedings{FormaliSE14p52,
author = {Jason Biatek and Michael W. Whalen and Mats P. E. Heimdahl and Sanjai Rayadurgam and Michael R. Lowry},
title = {Analysis and Testing of PLEXIL Plans},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {52--58},
doi = {},
year = {2014},
}
|
|
| Rossi, Matteo |
FormaliSE '14: "Flexible Modular Formalization ..."
Flexible Modular Formalization of UML Sequence Diagrams
Luciano Baresi, Mohammad Mehdi Pourhashem Kallehbasti, and Matteo Rossi (Politecnico di Milano, Italy) UML Sequence Diagrams are one of the most commonly used type of UML diagrams in practice. Their semantics is often considered to be straightforward, but a more detailed analysis reveals diverse interpretations. These different choices must be properly supported by verification tools. This paper describes a formal framework for capturing semantic choices in a precise and modular way. The user is then able to select the semantics of interest, mix different interpretations, and analyze diagrams according to the chosen solution. This solution is supported by Corretto, our UML verification environment, to allow the user to play with different semantics and prove properties on Sequence Diagrams, accordingly.
@InProceedings{FormaliSE14p10,
author = {Luciano Baresi and Mohammad Mehdi Pourhashem Kallehbasti and Matteo Rossi},
title = {Flexible Modular Formalization of UML Sequence Diagrams},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {10--16},
doi = {},
year = {2014},
}
|
|
| Sayar, Imen |
FormaliSE '14: "From an Abstract Specification ..."
From an Abstract Specification in Event-B toward an UML/OCL Model
Imen Sayar and Mohamed Tahar Bhiri (University of Sfax, Tunisia; University of Lorraine, France) The formal approach of software development promotes getting proved correct software. It faces the shortcomings of the classical approach concerning the ambiguity of the requirements document, the risk of errors distributed to all phases and the high testing cost (because of late detection of such errors). However, this approach poses problems mainly related to the participation of various actors not necessarily professionals in formal methods, maintenance and especially the development of an "optimal" refinement strategy. To overcome the limitations of these two approaches, we propose a hybrid approach that combines the formal approach (Event-B) and the classical approach (UML/OCL). Upstream phases of our approach include: Rewriting the requirements document, Refinement strategy, Abstract specification, Horizontal refinement and Validation. Downstream phases contain the Construction of a UML/EM-OCL model, Refinement, Integration of design and implementation decisions, Coding and Integration. In this paper, we show the feasibility of our approach on a case study: An Electronic Hotel Key System (SCEH). The problem of transition from formal (Event-B) to the semi-formal (UML/OCL) is processed by our OCL extension called EM-OCL.
@InProceedings{FormaliSE14p17,
author = {Imen Sayar and Mohamed Tahar Bhiri},
title = {From an Abstract Specification in Event-B toward an UML/OCL Model},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {17--23},
doi = {},
year = {2014},
}
|
|
| Shukla, Sandeep K. |
FormaliSE '14: "Compiling Polychronous Programs ..."
Compiling Polychronous Programs into Conditional Partial Orders for ASIP Synthesis
Mahesh Nanjundappa and Sandeep K. Shukla (Virginia Tech, USA) Synthesis of application specific hardware which minimizes area while not sacrificing latency or clock speed is a much researched problem. In most of the past works, the hardware is described structurally in hardware description languages with behaviors attached to structures. Since the structure is manually decided, the architect has to decide whether certain components can be reused without increasing latency. For example, if one can prove that certain behaviors never happen at the same time, these behaviors can be mapped to common components, with a simple control state machine determining which behavioral mode the behavior belongs to. Since application specific hardware are used as co-processors for performance boost, and such computations are best described as a data-flow computation (such as signal processing, encryption etc.,), we choose a high level data-flow oriented formal specification language, and use a new semantic model for this specification language, namely conditional partial order graphs. The advantage of our approach is that our specification language MRICDF is graphical, polychronous, has formal semantics, and hence synthesizing its control structure into conditional partial order is a natural fit. Additionally, the specific calculus of constraints in polychronous languages -- namely clock calculus, and associated analysis with Boolean theory of prime implicates, and constraint satisfiability checking with SMT solvers provide us with a natural way of discovering behaviors that belong to disjoint modes, and thereby allow us to reuse components with simple micro-instruction set synthesis. In this paper, we show how MRICDF can be used to formally synthesize such application specific instruction processors. Past approaches to synthesize hardware from the polychronous language SIGNAL were focused on synthesizing logic with hierarchical conditional dependency graphs as internal representation. Unlike those, we are synthesizing an application specific instruction set processor by automated synthesis of control and scheduling data-path.
@InProceedings{FormaliSE14p38,
author = {Mahesh Nanjundappa and Sandeep K. Shukla},
title = {Compiling Polychronous Programs into Conditional Partial Orders for ASIP Synthesis},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {38--44},
doi = {},
year = {2014},
}
|
|
| Simko, Gabor |
FormaliSE '14: "Formalization of Software ..."
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits (Vanderbilt University, USA) The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach.
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
|
|
| Sztipanovits, Janos |
FormaliSE '14: "Formalization of Software ..."
Formalization of Software Models for Cyber-Physical Systems
Sandeep Neema, Gabor Simko, Tihamer Levendovszky, Joseph Porter, Akshay Agrawal, and Janos Sztipanovits (Vanderbilt University, USA) The involvement of formal methods is indispensable for modern software engineering. This especially holds for Cyber-Physical Systems (CPS). In order to deal with the complexity and heterogeneity of the design, model-based engineering is widely used. The complexity of detailed verification in the final source code makes it imperative to introduce formal methods earlier in the design process. Because of the widespread use of customized modeling languages (domain-specific modeling languages, DSMLs), it is crucial to formally specify the DSML, and verify if the model meets fundamental correctness criteria. This is achieved by specifying behavioral and structural semantics of the modeling language. Significant model-driven tools have emerged incorporating advanced model checking methods that can provide some assurance regarding the quality and correctness of the models. However, the code generated from these models, using auto code generators remains circumspect, since the correctness of the code generators cannot be assumed as a given, and remains intractable to prove. Therefore, we propose a pragmatic approach, instead of verifying explicit implementation of code generator, verifies the correctness of the generated code with respect to a specific set of user-defined properties to establish that the code-generators are property-preserving. In order to make the verification workflow conducive to domain engineers, who are not often trained in formal methods, we include a mechanism for high-level specification of temporal properties using pattern-based verification templates. The presented toolchain leverages state-of-the-art verification tools, and a small case-study illustrates the approach.
@InProceedings{FormaliSE14p45,
author = {Sandeep Neema and Gabor Simko and Tihamer Levendovszky and Joseph Porter and Akshay Agrawal and Janos Sztipanovits},
title = {Formalization of Software Models for Cyber-Physical Systems},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {45--51},
doi = {},
year = {2014},
}
|
|
 |
Whalen, Michael W. |
FormaliSE '14: "Analysis and Testing of PLEXIL ..."
Analysis and Testing of PLEXIL Plans
Jason Biatek, Michael W. Whalen, Mats P. E. Heimdahl, Sanjai Rayadurgam, and Michael R. Lowry (University of Minnesota, USA; NASA Ames Research Center, USA) Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.
@InProceedings{FormaliSE14p52,
author = {Jason Biatek and Michael W. Whalen and Mats P. E. Heimdahl and Sanjai Rayadurgam and Michael R. Lowry},
title = {Analysis and Testing of PLEXIL Plans},
booktitle = {Proc.\ FormaliSE},
publisher = {ACM},
pages = {52--58},
doi = {},
year = {2014},
}
|
27 authors
proc time: 0.71