Google Summer of Code 2013

May 29th, 2013 by Jan

I am excited to announce that I have been accepted into a program that I have long been interested in: Google Summer of Code (GSoc). GSoC is a program where Google will provide money to student developers in order to contribute to open-source software. Many popular open-source projects are sponsored by the project, and each successful student is paired up with a (few) mentor(s). The student then works for the summer contributing code and advancing the project, and receives a cheque at the end of the summer (and a t-shirt).

Whether it’s because Google’s name is in the title, or because many people want to contribute to open-source software and get paid, or because big-name open-source projects participate, the project is very popular. In order to be accepted, students must submit an application to the (Google approved) open-source project of their choice. The application usually requires an outline of its goals or usefulness, a timeline, and expected deliverables. I suppose really good applications would go above-and-beyond this, and I would like to think, that to some extent, mine did as well (after all, it was accepted), but I’m not sure what I wrote which may not fall into one of these categories. That being said, my application was to NASA’s Java Pathfinder project, a Java-based model checker that is now being used to check Android software, but also includes a significant amount of work with the PRISM model checker. The idea is to leverage the strengths of both model checkers in order to verify probabilistic programs (e.g., programs that exhibit randomness).

I’m not quite sure I’m comfortable talking about the project in greater detail yet, mostly because I’m not sure how many of those details I’m sure of at this moment. That being said, I am really excited about the project, and I have been spending my days getting familiar with the various code structures that I’ll be working with, in addition to reading papers that are related to the work, or that aren’t but still look interesting. I have also started a blog that I’m going to post project-specific updates to daily, mostly to track my projects, but also to explain ideas to an imaginary crowd in order to make sure that I understand them. Feel free to check it out, but if you’re less concerned with the details, wait until the end of the summer, when I will post a summary of the project on this blog. Regardless, I hope the project goes well and relates back to my more academic goals (as opposed to my “develop software” goals, if I really have any). In particular, I would love to get a research paper out of the work, rather than simply contributing code. Assuming things go well, I am hard pressed as to come up with reasons why this would not be the case; certainly model checking is a very active area of research, and one that I am not entirely new to (not that I want to imply I’ve had any real results in proper model checking). I’m hoping there will be be something to publish somewhere, as that would be really great.

Defining a Model

May 25th, 2011 by Jan

In formal methods and other areas of computer science and software engineering (e.g., model driven engineering), models are a common occurrence. But despite their use, models are hard to define. Many people have sought out to define and characterize what constitutes a model and this post will review some of these characterizations.

The first notions of a model that will be considered come from Thomas Kühne in 2005. He starts by suggesting that in the past, models have generally been artifacts developed in a modelling language, but more recently, even Java programs have been considered models [1]. After reviewing the ideas of a few other discussions on the topic (namely, those put forth by Stachowiak and Steinmüller), Kühne suggests that models should be a projection (which is a reduction) of an original and that they must be exact–but not complete. Models must not copy the object being modeled, and Kühne dedicates a section to arguing that a copy is not a model. A copy allows for “test runs” rather than model simulations. However, models must still be exact with respect to the properties that are being modeled.

Interestingly, and perhaps counter-intuitively to many, Kühne suggests that models are not (necessarily) a description of the source object. Indeed, some models fail to describe the system they are modeling, as they only model a few interesting properties of it. Though I do agree, I think Kühne should have noted explicitly that models often do describe the systems they represent. Kühne however proceeds to talk about two types of models, ones that are used in the design phase of software, and ones that are used in the analysis phase of software. In doing this, Kühne admits that some models describe problems. He also notes that the source object being modeled may be theoretical, as in the case of models used in the design phases of software development.

The remainder of Kühne’s paper discusses metamodels. The discussion arises from the fact that there a two fundamentally different types of models that can result in the term metamodel (and others) to be misunderstood. The two types are token models and type models [1].

Token models are models that capture a “single configuration” and represent single object instances with their elements [1]. Kühne notes that the relation “representation of” is transitive for token models. An instance of an instance representing an object, is still an representation of the original model; the paper uses a map example with varying map scales to clarify. The transitivity property of the “representation of” relation should determine when the prefix meta- should be applied to a model–and it doesn’t make sense for models that are related by a transitive operation like “representation of”. Thus two token models representing instances of the same object are two models; neither of them are metamodels. A model of a token model is a metamodel if it models the token model’s properties, rather than its contents. Type models capture “universal aspects” of an original object. Furthermore, type models show only types of interest. A UML class diagram is an example of a type model.

Lastly, Kühne clarifies the notion that a true metamodel can always be understood as a language definition, and that metamodels should still be considered models. Metamodels are token models with reduction features of the language that they model, and are potentially type models that can describe all models that would be represented by the metamodel.

In a paper by Pierre-Alain Muller et al., “Modeling Modeling,” the author suggests that software engineers have been using models without knowing it. In particular, there is a hidden relation that modelers rely on that the authors explicate. The paper focuses primarily on this relation after relatively small a section on model definitions.

The definitions considered however, represent a varying understanding and are considered briefly in subsections. The first such subsection lists features that models should have, which are represented fairly well by the notions described above by Kühne: projection and exactness, though in greater detail. The ideas stem from Stachowiak (again) and Bran Selic, though Selic interestingly also lists understandability and inexpensiveness while Stachowiak makes the notion of a mapping explicit. However, as models are not supposed to be copies, I suspect that many people would presume that they are cheaper and that inexpensiveness is implicit. The next subsection describes kinds of models, listing ideas from Seidewitz and Favre that largely overlap: a distinction of descriptive and specification models, which was touched on briefly by Kühne, and ends with Kühne’s distinction of type and token models.

Next, a model of modelling is developed. The authors aim to “designate a representation of what we manipulate when we use modeling techniques” [2]. Abstracting away the details of models, the authors consider “things” and “arrows,” which are roughly objects and relations, citing a foundation in Category Theory. The arrow graphics are manipulated by changing shape (straight to wavey, for example) and result in expressing different types of relations between two objects and their intention. An object’s intention is what the term implies: the give purpose it exists to fulfill. Using labels on the arrows of the representation of relation, notions such as descriptive and specification models can be expressed. The term causality is also introduced, which communicates when a descriptive model is correct and a specification model is valid. To cover transitivity in modeling models, a framework is established that allows for combinations to have multiple outputs depending on the inputs of models and their intentions.

The remainder of this paper deals with examples that primarily serve to display the new notation. These examples will not be covered here, and interested readers should seek them in [2].

Lastly, we consider the work of Jochen Ludewig, who provides an introduction to models in software engineering [3]. Again, Stachowiak’s criteria come up as a basis for model definitions. This time, however, they are examined with greater depth than in the papers previously considered. In particular, there is an emphasis on models that are practical when the original is not, and that though models are reduction of the original, they often include additional attributes, which Ludewig calls abundant attributes, that present in the model but not in the original. These attributes often allow the model to be useful and Ludewig gives an example of Z syntax as possible abundant attributes.

Unlike the other papers, Ludewig also considers terms that are related to “model”. Namely, tool, icon, name, metaphor, and theory. Ludewig argues that the use of tool and name should not be similar to that of a model; tools lose their relationship to any original as tools evolve, and names do not provide information about an object. Icons (or symbols) are similarly not models: they do not provide information, except in a few cases, and even then the amount of information provided is not substantial. Metaphors and theories on the other hand, are models. Metaphors are a models because the comparison (usually) reveals some information about the original, and are particularly useful for new entities. Theories are abstract models that emphasize “results and conclusions rather than obviousness” [3].

Ludewig also mentions the notions of prescriptive (specification) and descriptive models; these are not new terms by now. However, Ludewig introduces the term transient models for models that are both at different times. Furthermore, Ludewig emphasizes that descriptive models do not need to come after the original. In using an example of a weather describing model, Ludewig shows that such a descriptive model can describe the behaviour of upcoming weather before it happens. Note that this is not a specification model: the weather was not created due to the model.

Next, Ludewig goes on to describe purposes of models, saying that such purposes can be used to classify models. Models can be used as documentation or to provide instructions, as exploratory entities used to simulate changes, as practical replacements for originals in an educational manner, or as formal “mathematical” models (e.g. the formulas used in physics and chemistry) [3].

Ludewig then considers the role of some of these classifications in software engineering. In particular, he claims that models in software engineering are primarily prescriptive; models in software engineering generally have the end goal of code in mind. One exception that Ludewig points out is a requirements document: while it is true that it is a prescriptive model for other development documents, it is also a descriptive model of the user’s needs. Additionally, since models often prescribe other models in software engineering, Ludewig reminds the reader that at each prescription, some information is lost, and in order to keep systems consistent, tracing should be possible. Tracing is the “identification” of modifications in different models when the models that describe them change [3]. Backward tracing is also possible.

Beyond this, Ludewig argues that since the systems used in software engineering only mimic the existing world, software engineering is limited. In particular, systems that “depart” from traditional models are some of the greatest engineering achievements, and this is not common in software systems. A few exceptions are noted, such as quicksort, which is quite fast on a system but not commonly performed by hand. However, Ludewig has hope that eventually models of software development will be sufficiently well understood that such breakthroughs will be more common, but believes there is much work to be done before that occurs. Ludewig also notes that there are risks from using models in software engineering (and elsewhere): people often look for faults in reality, rather than faults in their models. In order to advance the state of software engineering, Ludewig and his research group have developed a system called Software Engineering Simulation using Animated Models (SESAM). The system is briefly described in the paper and aims to simulate software engineering in a manner similar to simulating flight for a pilot. However, in this case, the “pilot” is a project manager for a software project. After some use, the system revealed that descriptive models are difficult to work with, for example, compromises of realism for simplicity.

Switching back to a focus on prescriptive models, Ludewig says that while they are easy to develop, they are hard to test. Notably, Ludewig says that most research projects do not go far enough after conception to demonstrate their superiority or applicability. He concludes by saying research on comparing existing ideas should be more common in order to counter this problem.

In conclusion, there are various notions that a good model should satisfy. Some of the more common ones have been visited above, namely the need for a reduction, mapping, and practicality. They should also be accurate with respect to the properties they model. Models can further be classified as specification, descriptive, or transient, and by the purpose they serve. Models can also be modeled as metamodels, provided they model properties and not the content of the original model. Hopefully the definitions considered have clarified (or confirmed) your own notions.

Read the rest of this entry »

NSERC USRA Advice

May 18th, 2011 by Jan

I was fortunate enough to hold an NSERC USRA position during my undergraduate career, and as a result, I was occasionally asked how I found such an opportunity. This post should explain the process and give a few tips for finding a supervisor. USRAs are a great way to gain valuable research experience before graduate studies and explore academia beyond the classroom.

First, be prepared to look outside your home institution. While there may be many potential supervisors at your home university, each university typically receives a limited number of awards. Applying to supervisors at other institutions increases your chances of securing a position. Furthermore, these departments may also pay out of pocket for students that are ineligible for USRAs, such as international students (for example, I know the University of Toronto Department of Computer Science and the University of Waterloo Department of Combinatorics & Optimization will do this if you cannot secure an NSERC award). The only catch is that you won’t be able to tell people you held an NSERC award, though the pay and research will be the same and still worth the time.

Second, start early. Departmental and university deadlines vary, but most are in January or February for summer (May-August) positions. Some are earlier but I found looking for positions around the first week of January resulted in the majority of deadlines being met.

Third, don’t wait for departmental invites, approach professors. Many professors have projects waiting around for students to work on, but don’t have the time to advertise, or their department doesn’t have enough professors with projects to put out a call for students. Seek professors with related research interests and send them an email or approach them to discuss potential projects. I found professors who listed supervised students the most likely to respond, but others that didn’t list any students would often also respond. If possible, check to see if the professor’s university has any specific in house rules for obtaining an award. For example, the University of Waterloo requires an “A-” average (80%) for consideration while the award only requires a “B” (73-76%). These aren’t always a major concern, especially if the professor can work something out with the university–though this usually requires you to be particularly suited for the position. Do make sure you meet the eligibility criteria for the award as described by NSERC–these are necessary. I would say that you should take special care to seek professors who have NSERC grants, but most professors have them so you probably don’t need to watch out for it. In the worst case, you’ll be informed that they aren’t supported by NSERC and you should move on. Regardless, when you approach professors, bring or email a copy of your undergraduate transcript and your resume. In most cases, an unofficial transcript will suffice. Lastly, know departmental deadlines and rules in case the professors haven’t supervised a student recently or before; it save them work and I’ve been asked before.

If your project seems promising and you’re invited to apply, make sure you supply the professor, his or her department, or the university’s department of research services or graduate studies with the appropriate documents. Such documents will include NSERC Form 202 Part I and might include a questionnaire, or an official copy of your transcript (like the University of British Columbia’s Department of Mathematics), so it might be wise to order a few in advance of applications. Your supervisor will have to fill out Form 202 Part II and reference your application, so make sure you fill out Part I online and provide your professor with the reference number. You will need to print out, sign, and deliver a hard copy of the form in most cases. If you’re applying to an institution you’re not familiar with, it may be possible to mail this document to your professor to hand in along with their Form 202 Part II in order to ensure it goes to the correct people.

Fourth, make sure you apply to multiple institutions. Sometimes a professor will want to work with you but the institution will not grant you the award. Make sure to send multiple applications out unless you know you’ve got a position secured. Be sure to inform your potential supervisors of this: it means theres a chance you won’t be working for them, and some departments want to know if you’ve applied elsewhere.

Lastly, I’ve included a list of departments and institutions below that actively invite students to be considered for NSERC USRA positions (usually summer positions). Note that they currently focus on mathematics and computer science departments as these were my primary areas of study, so I apologize. If you’re reading this and know of other departments or institutions that advertise open positions, send me an e-mail and I’ll add it to the list.

Good luck!

Read the rest of this entry »

An Introduction to Modelling Notations in Model Based Software Engineering: Alloy & Statecharts

May 17th, 2011 by Jan

In this post, I’m going to briefly describe two notations for models that are popular in model based software engineering. The first, Alloy, is a relatively new language while the second, statecharts, are much older.

Alloy was developed by Daniel Jackson at MIT, who published the first paper on the language in 2001, titled “Alloy: a lightweight object modelling notation.” Jackson created the language as a tool for lightweight formal methods: reduced cost formal methods with the benefits of “traditional” formal methods. Heavily inspired by Z, Alloy is a small expressive, declarative, language that can express useful structural properties of models. That means Alloy is designed for models that model what affects are achieved, rather than models that model how such affects are achieved. Primarily a model-finder (rather than a model-checker), Alloy, through the use of the Alloy Analyzer, finds and displays state snapshots of models. Such snapshots can be considered pre- and post-states, allowing Alloy to describe the behaviour of models. A user can constrain the outputs to instances that satisfy predicates.

The Alloy Analyzer is a tool used to find instances of the system modeled (typically constrained by predicates), as well as find counter-examples to assertions regarding the model. Asserts are written in the model and the Analyzer will check exhaustively for instances that satisfy the model constraints and violate the assertion. This is done through restricting the scope of the instances to be checked. The Analyzer will exhaustively search every possible instance where there is at most scope number of elements in each set of objects. Jackson’s motivation for this is his small scope hypothesis: most errors do not require many instances of objects, and can be found by considering relations on only a few objects. Thus a scope of 3 or 4 will often reveal flaws in models, and since the Analyzer is complete and sound, all such errors with at most 3 (or 4) objects of each type will be reported and the Analyzer won’t report any false negative. On a typical computer, such a search is quick (a few milliseconds for small models) but with larger models and slower machines this can vary. Interestingly, the Analyzer works by translating the model and constraints to a long SAT formula, which is then fed to an off-the shelf SAT solver, capitalizing on the research advances in solving SAT problems. This means performance gains are possible by switching the underlying SAT solver. The Analyzer also supports the generation of metamodels and themes, to customize how model instances (and metamodels) are displayed.

The language itself has both a graphical and textual syntax, though the use of the Analyzer requires textual input. Alloy has no explicit types, and is built on sets and relations. It should be noted that the (textual) syntax of the language has changed greatly since Jackson’s first paper. A tutorial for Alloy can be found here.

In contrast to Alloy, Statecharts are older and much more familiar (provided the reader has any background in modelling or more generally, software engineering). Statecharts were introduced in 1987 by David Harel. A primarily graphical system of modelling systems, statecharts look similar (though often more complicated than) finite state machines. Harel’s goal in designing statecharts was to have a system that could represent concurrency, allow grouping of common actions, and present different levels of abstraction while ensuring all properties were formally defined. Though statecharts look similar to finite state machines, they often have many new features that Harel introduced: superstates, that allow for state composition and a state to have a substate; (deep) history to allow the system to remember what substate it is in when the superstate exits; conditional and selectional connectives to control the flow of the machine entering a state with substates; actions and activities: processes run by the system which are instantaneous and long-lived, respectively; timeouts and more. By using superstates, the level of abstraction can vary: the contents of the superstate may not be required for someone looking at the big picture, while particular developers can expose and inspect the superstate’s internals.

The full paper on statecharts, though dated, is an excellent introduction. Statecharts do have pitfalls though, and the paper mentions at least two. They are not particularly suited for simultaneous events (though concurrent events are supported, and thus many simultaneous events are modeled quite well, however, not all simultaneous event are suited for statecharts), and there are occasionally possibilities of non-determinism that are cause for concern. More current research may have formalized resolutions for these problems, but I don’t have any references to confirm this, and I suspect that often modelers simply agree on a behaviour if an inconsistency might arise.

Read the rest of this entry »

New Site

July 13th, 2010 by Jan

Welcome to my new site. It’s still a work in progress, but I’ve got links to my resume and a quick biography set up. Feel free to take a look around.