{"id":2906,"date":"2019-11-22T09:43:43","date_gmt":"2019-11-22T09:43:43","guid":{"rendered":"https:\/\/emadridnet.uc3m.es\/?p=2906"},"modified":"2021-12-09T09:45:18","modified_gmt":"2021-12-09T09:45:18","slug":"learning-formal-specification-should-also-be-fun","status":"publish","type":"post","link":"https:\/\/emadridnet.uc3m.es\/en\/2019\/11\/22\/learning-formal-specification-should-also-be-fun\/","title":{"rendered":"\u00abLearning formal specification should also be fun\u00bb"},"content":{"rendered":"<p>[et_pb_section fb_built=&#8221;1&#8243; fullwidth=&#8221;on&#8221; admin_label=&#8221;Header&#8221; _builder_version=&#8221;3.22&#8243; background_image=&#8221;https:\/\/emadridnet.uc3m.es\/wp-content\/uploads\/sites\/40\/2021\/05\/meetup-02.jpg&#8221; parallax=&#8221;on&#8221; custom_padding=&#8221;|||&#8221; animation_style=&#8221;slide&#8221; animation_direction=&#8221;top&#8221; animation_intensity_slide=&#8221;2%&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_fullwidth_header title=&#8221;\u00abLearning formal specification should also be fun\u00bb&#8221; subhead=&#8221;Wishnu Prasetya&#8221; button_one_text=&#8221;Free Registration&#8221; button_one_url=&#8221;https:\/\/www.eventbrite.es\/e\/81290902277&#8243; background_overlay_color=&#8221;rgba(255,255,255,0.6)&#8221; content_max_width=&#8221;700px&#8221; content_max_width_tablet=&#8221;100%&#8221; content_max_width_phone=&#8221;&#8221; content_max_width_last_edited=&#8221;on|desktop&#8221; _builder_version=&#8221;4.14.1&#8243; title_font=&#8221;Roboto|300|||||||&#8221; title_font_size=&#8221;60px&#8221; title_line_height=&#8221;1.4em&#8221; content_font=&#8221;||||||||&#8221; content_font_size=&#8221;17px&#8221; content_line_height=&#8221;1.9em&#8221; subhead_font=&#8221;|600|||||||&#8221; subhead_font_size=&#8221;20px&#8221; subhead_line_height=&#8221;1.8em&#8221; background_color=&#8221;rgba(158,158,158,0.3)&#8221; background_image=&#8221;https:\/\/storage.googleapis.com\/wp-uploads.bucket.wp.uc3m.es\/wp-content\/uploads\/sites\/40\/2021\/11\/26092203\/GetImage.jpg&#8221; custom_button_one=&#8221;on&#8221; button_one_text_size=&#8221;14px&#8221; button_one_text_color=&#8221;#ffffff&#8221; button_one_bg_color=&#8221;#8300e9&#8243; button_one_bg_color_gradient_start=&#8221;#d883f8&#8243; button_one_bg_color_gradient_end=&#8221;#352DBE&#8221; button_one_bg_color_gradient_direction=&#8221;90deg&#8221; button_one_border_width=&#8221;10px&#8221; button_one_border_color=&#8221;rgba(0,0,0,0)&#8221; button_one_border_radius=&#8221;100px&#8221; button_one_letter_spacing=&#8221;3px&#8221; button_one_font=&#8221;Roboto|700||on|||||&#8221; custom_button_two=&#8221;on&#8221; button_two_text_size=&#8221;14px&#8221; button_two_text_color=&#8221;#ffffff&#8221; button_two_bg_color=&#8221;#06c8ff&#8221; button_two_border_width=&#8221;10px&#8221; button_two_border_color=&#8221;rgba(0,0,0,0)&#8221; button_two_border_radius=&#8221;100px&#8221; button_two_letter_spacing=&#8221;3px&#8221; button_two_font=&#8221;Roboto|700||on|||||&#8221; background_layout=&#8221;light&#8221; custom_margin=&#8221;||||false&#8221; custom_padding=&#8221;8vw||8vw||true&#8221; custom_padding_tablet=&#8221;250px||250px||true&#8221; custom_padding_last_edited=&#8221;off|desktop&#8221; link_option_url_new_window=&#8221;on&#8221; hover_enabled=&#8221;0&#8243; title_font_size_tablet=&#8221;40px&#8221; title_font_size_phone=&#8221;32px&#8221; title_font_size_last_edited=&#8221;on|desktop&#8221; button_one_text_color_hover=&#8221;#ffffff&#8221; button_two_text_color_hover=&#8221;#ffffff&#8221; button_one_letter_spacing_hover=&#8221;3px&#8221; button_two_letter_spacing_hover=&#8221;3px&#8221; global_colors_info=&#8221;{}&#8221; button_one_text_size__hover_enabled=&#8221;off&#8221; button_two_text_size__hover_enabled=&#8221;off&#8221; button_one_text_color__hover_enabled=&#8221;on&#8221; button_one_text_color__hover=&#8221;#ffffff&#8221; button_two_text_color__hover_enabled=&#8221;on&#8221; button_two_text_color__hover=&#8221;#ffffff&#8221; button_one_border_width__hover_enabled=&#8221;off&#8221; button_two_border_width__hover_enabled=&#8221;off&#8221; button_one_border_color__hover_enabled=&#8221;off&#8221; button_two_border_color__hover_enabled=&#8221;off&#8221; button_one_border_radius__hover_enabled=&#8221;off&#8221; button_two_border_radius__hover_enabled=&#8221;off&#8221; button_one_letter_spacing__hover_enabled=&#8221;on&#8221; button_one_letter_spacing__hover=&#8221;3px&#8221; button_two_letter_spacing__hover_enabled=&#8221;on&#8221; button_two_letter_spacing__hover=&#8221;3px&#8221; button_one_bg_color__hover_enabled=&#8221;off&#8221; button_two_bg_color__hover_enabled=&#8221;off&#8221; theme_builder_area=&#8221;post_content&#8221; title_text=&#8221;GetImage&#8221; sticky_enabled=&#8221;0&#8243;][\/et_pb_fullwidth_header][\/et_pb_section][et_pb_section fb_built=&#8221;1&#8243; admin_label=&#8221;Visiting&#8221; _builder_version=&#8221;3.22&#8243; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_row _builder_version=&#8221;3.25&#8243; custom_padding=&#8221;27px|0px|24px|0px|false|false&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;3.25&#8243; custom_padding=&#8221;|||&#8221; global_colors_info=&#8221;{}&#8221; custom_padding__hover=&#8221;|||&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_text _builder_version=&#8221;4.14.1&#8243; text_font=&#8221;||||||||&#8221; text_font_size=&#8221;16px&#8221; text_line_height=&#8221;1.9em&#8221; header_font=&#8221;||||||||&#8221; header_2_font=&#8221;Roboto|300|||||||&#8221; header_2_font_size=&#8221;50px&#8221; header_2_line_height=&#8221;1.4em&#8221; hover_enabled=&#8221;0&#8243; header_2_font_size_tablet=&#8221;40px&#8221; header_2_font_size_phone=&#8221;32px&#8221; header_2_font_size_last_edited=&#8221;on|phone&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221; sticky_enabled=&#8221;0&#8243;]<\/p>\n<h2 style=\"text-align: justify\">Abstract<\/h2>\n<p style=\"text-align: justify\"><span>There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This talk will present a game called FormalZ that teachers can use to introduce some variation in their class. Students can have some fun in playing the game and, while doing so, also learn the basics of writing formal specifications. Unlike existing software engineering themed education games, FormalZ takes a rather radical approach, namely deep gamification where playing gets a more central role in order to generate more engagement. We will discuss the results of our field study with this game, what we learned from this study and our recommendation for future work.\u00a0<\/span><\/p>\n<p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=&#8221;1&#8243; admin_label=&#8221;About&#8221; _builder_version=&#8221;3.22&#8243; min_height=&#8221;677px&#8221; custom_margin=&#8221;-3px|||||&#8221; custom_padding=&#8221;0px|||||&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_row column_structure=&#8221;1_2,1_2&#8243; padding_top_bottom_link_1=&#8221;true&#8221; padding_left_right_link_1=&#8221;true&#8221; _builder_version=&#8221;4.9.4&#8243; min_height=&#8221;509.8px&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_column type=&#8221;1_2&#8243; _builder_version=&#8221;3.25&#8243; background_image=&#8221;https:\/\/storage.googleapis.com\/wp-uploads.bucket.wp.uc3m.es\/wp-content\/uploads\/sites\/40\/2021\/05\/28095053\/column-background-02.png&#8221; custom_padding=&#8221;50px|50px|50px|50px&#8221; custom_padding_tablet=&#8221;&#8221; custom_padding_phone=&#8221;20px|20px|20px|20px|true|true&#8221; custom_padding_last_edited=&#8221;on|phone&#8221; global_colors_info=&#8221;{}&#8221; padding_phone=&#8221;20px|20px|20px|20px|true|true&#8221; padding_last_edited=&#8221;on|phone&#8221; custom_padding__hover=&#8221;|||&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_image src=&#8221;https:\/\/storage.googleapis.com\/wp-uploads.bucket.wp.uc3m.es\/wp-content\/uploads\/sites\/40\/2021\/11\/26092203\/GetImage.jpg&#8221; title_text=&#8221;GetImage&#8221; align_tablet=&#8221;center&#8221; align_phone=&#8221;&#8221; align_last_edited=&#8221;on|desktop&#8221; _builder_version=&#8221;4.14.1&#8243; animation_style=&#8221;zoom&#8221; animation_intensity_zoom=&#8221;10%&#8221; hover_enabled=&#8221;0&#8243; box_shadow_style=&#8221;preset1&#8243; box_shadow_vertical=&#8221;32px&#8221; box_shadow_blur=&#8221;100px&#8221; box_shadow_color=&#8221;rgba(0,0,0,0.15)&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221; sticky_enabled=&#8221;0&#8243;][\/et_pb_image][\/et_pb_column][et_pb_column type=&#8221;1_2&#8243; _builder_version=&#8221;3.25&#8243; custom_padding=&#8221;|||&#8221; custom_padding_tablet=&#8221;0px|||&#8221; custom_padding_last_edited=&#8221;off|desktop&#8221; global_colors_info=&#8221;{}&#8221; padding_tablet=&#8221;0px|||&#8221; padding_last_edited=&#8221;off|desktop&#8221; custom_padding__hover=&#8221;|||&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_text _builder_version=&#8221;4.14.1&#8243; text_font=&#8221;||||||||&#8221; text_font_size=&#8221;16px&#8221; text_line_height=&#8221;1.9em&#8221; header_font=&#8221;||||||||&#8221; header_2_font=&#8221;Roboto|300|||||||&#8221; header_2_font_size=&#8221;50px&#8221; header_2_line_height=&#8221;1.4em&#8221; hover_enabled=&#8221;0&#8243; header_2_font_size_tablet=&#8221;40px&#8221; header_2_font_size_phone=&#8221;32px&#8221; header_2_font_size_last_edited=&#8221;on|phone&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221; sticky_enabled=&#8221;0&#8243;]<\/p>\n<h2>Biograf\u00eda<\/h2>\n<p style=\"text-align: justify\"><span>S.W.B. (Wishnu) Prasetya is researcher and lecturer at the Department of Information and Computing Sciences, Utrecht University. His field of research is software testing and verification. actively conducts research in the field of software testing and verification. In the past ten years he has been lecturing in courses such as Modelling and System Development, Software Testing and Verification, ICT Entrepreneurship, and Software Project. He investigates ways to use computers to test software, so that the burden of manual work can be reduced and, hence producing better quality software while reducing the cost. He is also the author and maintainer of the tool T3, which is an automated random-based testing tool to test Java classes (https:\/\/git.science.uu.nl\/prase101\/t3\/wikis\/home).<\/span><\/p>\n<p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=&#8221;1&#8243; admin_label=&#8221;Past Events&#8221; _builder_version=&#8221;3.22&#8243; background_image=&#8221;https:\/\/emadridnet.uc3m.es\/wp-content\/uploads\/sites\/40\/2021\/05\/bg-4.png&#8221; background_size=&#8221;initial&#8221; background_position=&#8221;bottom_left&#8221; min_height=&#8221;936.3px&#8221; custom_padding=&#8221;1px|0px|0|0px|false|false&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_row _builder_version=&#8221;3.25&#8243; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;3.25&#8243; custom_padding=&#8221;|||&#8221; global_colors_info=&#8221;{}&#8221; custom_padding__hover=&#8221;|||&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_text _builder_version=&#8221;3.27.4&#8243; text_font=&#8221;||||||||&#8221; text_font_size=&#8221;16px&#8221; text_line_height=&#8221;1.9em&#8221; header_font=&#8221;||||||||&#8221; header_2_font=&#8221;Roboto|300|||||||&#8221; header_2_font_size=&#8221;50px&#8221; header_2_line_height=&#8221;1.4em&#8221; text_orientation=&#8221;center&#8221; header_2_font_size_tablet=&#8221;40px&#8221; header_2_font_size_phone=&#8221;32px&#8221; header_2_font_size_last_edited=&#8221;on|phone&#8221; locked=&#8221;off&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;]<\/p>\n<h2>Video<\/h2>\n<p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row custom_padding_last_edited=&#8221;on|phone&#8221; _builder_version=&#8221;3.25&#8243; background_image=&#8221;https:\/\/storage.googleapis.com\/wp-uploads.bucket.wp.uc3m.es\/wp-content\/uploads\/sites\/40\/2021\/05\/28095101\/column-background-03-1.png&#8221; min_height=&#8221;287px&#8221; custom_margin=&#8221;-11px|auto||auto||&#8221; custom_padding=&#8221;0px|50px|0|50px|false|false&#8221; custom_padding_tablet=&#8221;&#8221; custom_padding_phone=&#8221;20px|20px||20px||true&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;3.25&#8243; custom_padding=&#8221;|||&#8221; global_colors_info=&#8221;{}&#8221; custom_padding__hover=&#8221;|||&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_video src=&#8221;https:\/\/vimeo.com\/386448944&#8243; play_icon_color=&#8221;#000000&#8243; _builder_version=&#8221;4.14.1&#8243; animation_style=&#8221;zoom&#8221; animation_direction=&#8221;bottom&#8221; animation_intensity_zoom=&#8221;10%&#8221; animation_starting_opacity=&#8221;100%&#8221; hover_enabled=&#8221;0&#8243; box_shadow_style=&#8221;preset1&#8243; box_shadow_vertical=&#8221;32px&#8221; box_shadow_blur=&#8221;100px&#8221; box_shadow_color=&#8221;rgba(0,0,0,0.15)&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221; sticky_enabled=&#8221;0&#8243;][\/et_pb_video][\/et_pb_column][\/et_pb_row][et_pb_row _builder_version=&#8221;4.9.4&#8243; _module_preset=&#8221;default&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;4.9.4&#8243; _module_preset=&#8221;default&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_text _builder_version=&#8221;3.27.4&#8243; text_font=&#8221;||||||||&#8221; text_font_size=&#8221;16px&#8221; text_line_height=&#8221;1.9em&#8221; header_font=&#8221;||||||||&#8221; header_2_font=&#8221;Roboto|300|||||||&#8221; header_2_font_size=&#8221;50px&#8221; header_2_line_height=&#8221;1.4em&#8221; text_orientation=&#8221;center&#8221; header_2_font_size_tablet=&#8221;40px&#8221; header_2_font_size_phone=&#8221;32px&#8221; header_2_font_size_last_edited=&#8221;on|phone&#8221; locked=&#8221;off&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;]<\/p>\n<h2>Slides<\/h2>\n<p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row _builder_version=&#8221;4.9.4&#8243; _module_preset=&#8221;default&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;4.9.4&#8243; _module_preset=&#8221;default&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_video_slider _builder_version=&#8221;4.14.1&#8243; _module_preset=&#8221;default&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221;][et_pb_video_slider_item src=&#8221;https:\/\/www.slideshare.net\/emadridnet\/22112019-learning-formal-specification-should-also-be-fun-by-wishnu-prasetya&#8221; _builder_version=&#8221;4.14.1&#8243; _module_preset=&#8221;default&#8221; global_colors_info=&#8221;{}&#8221; theme_builder_area=&#8221;post_content&#8221; show_image_overlay=&#8221;off&#8221;][\/et_pb_video_slider_item][\/et_pb_video_slider][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Abstract There are many benefits in providing formal specifications for our software. However, teaching students to do this is not always easy as courses on formal methods are often experienced as dry by students. This talk will present a game called FormalZ that teachers can use to introduce some variation in their class. Students can [&hellip;]<\/p>\n","protected":false},"author":82,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"","_et_gb_content_width":"","footnotes":""},"categories":[28],"tags":[],"class_list":["post-2906","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"_links":{"self":[{"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/posts\/2906","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/users\/82"}],"replies":[{"embeddable":true,"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/comments?post=2906"}],"version-history":[{"count":2,"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/posts\/2906\/revisions"}],"predecessor-version":[{"id":2909,"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/posts\/2906\/revisions\/2909"}],"wp:attachment":[{"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/media?parent=2906"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/categories?post=2906"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/emadridnet.uc3m.es\/en\/wp-json\/wp\/v2\/tags?post=2906"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}